summaryrefslogtreecommitdiff
path: root/Jennisys
diff options
context:
space:
mode:
authorGravatar Aleksandar Milicevic <unknown>2011-08-02 18:03:05 -0700
committerGravatar Aleksandar Milicevic <unknown>2011-08-02 18:03:05 -0700
commit3e495e729cc68e2bfb1ab1c5cf11d38b2450f0e6 (patch)
treee0082cb8defff32ff2835048342c16132d6dfb04 /Jennisys
parent4851c9615e5e5267c86e43ae578fa23971fb372d (diff)
Jennisys: implemented a unification algorithm that tries to find an existing
method that matches (specification-wise) a synthesized one
Diffstat (limited to 'Jennisys')
-rw-r--r--Jennisys/Jennisys/Analyzer.fs198
-rw-r--r--Jennisys/Jennisys/AstUtils.fs117
-rw-r--r--Jennisys/Jennisys/Jennisys.fsproj2
-rw-r--r--Jennisys/Jennisys/Printer.fs8
-rw-r--r--Jennisys/Jennisys/Utils.fs17
-rw-r--r--Jennisys/Jennisys/examples/List2.jen6
-rw-r--r--Jennisys/Jennisys/examples/Set.jen21
-rw-r--r--Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy139
-rw-r--r--Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy213
-rw-r--r--Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy393
-rw-r--r--Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy233
-rw-r--r--Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy269
12 files changed, 1527 insertions, 89 deletions
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 103b7350..fff6b395 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -13,14 +13,19 @@ open Utils
open Microsoft.Boogie
+// =======================================================================
+/// Merges two solution maps so that if there are multiple entries for a
+/// single (comp,method) pair it concatenates them (corresponds to multiple
+/// branches).
+// =======================================================================
let MergeSolutions sol1 sol2 =
let rec __Merge sol1map sol2lst res =
match sol2lst with
| ((c2,m2), lst2) :: rest ->
- match sol1map |> Map.tryFindKey (fun (c1,m1) lst1 -> GetComponentName c1 = GetComponentName c2 && GetMethodName m1 = GetMethodName m2) with
+ match sol1map |> Map.tryFindKey (fun (c1,m1) lst1 -> CheckSameMethods (c1,m1) (c2,m2)) with
| Some(c1,m1) ->
let lst1 = sol1map |> Map.find(c1,m1)
- let newRes = res |> Map.add (c1,m1) (lst1 @ lst2)
+ let newRes = res |> Map.add (c1,m1) (lst1@lst2)
__Merge sol1map rest newRes
| None ->
let newRes = res |> Map.add (c2,m2) lst2
@@ -303,6 +308,8 @@ let GetHeapExpr prog mthd heapInst =
// ------------------------------- Modularization stuff ---------------------------------
+exception CannotUnify
+
let GetModularBranch prog comp meth hInst =
let rec __AddDirectChildren e acc =
match e with
@@ -310,11 +317,14 @@ let GetModularBranch prog comp meth hInst =
| SequenceExpr(elist)
| SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc
| _ -> acc
+
let __GetDirectChildren =
let thisRhsExprs = hInst.assignments |> List.choose (function ((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None)
thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty
|> Set.toList
+
let directChildren = lazy (__GetDirectChildren)
+
let __IsAbstractField ty var =
let builder = CascadingBuilder<_>(false)
let varName = GetVarName var
@@ -323,6 +333,16 @@ let GetModularBranch prog comp meth hInst =
let! fld = GetAbstractFields comp |> List.fold (fun acc v -> if GetVarName v = varName then Some(varName) else acc) None
return true
}
+
+ let __FindObj objName =
+ try
+ hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst
+ with
+ | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)
+
+ let __GetObjLitType objLitName =
+ (__FindObj objLitName).objType
+
let __GetAbsFldAssignments objLitName =
hInst.assignments |> List.choose (fun ((obj,var),e) ->
if obj.name = objLitName && __IsAbstractField obj.objType var then
@@ -349,6 +369,7 @@ let GetModularBranch prog comp meth hInst =
let __GetSpecFor objLitName =
let absFieldAssignments = __GetAbsFldAssignments objLitName
absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral
+
let __GetArgsUsed expr =
let args = GetMethodArgs meth
let argSet = DescendExpr2 (fun e acc ->
@@ -360,34 +381,145 @@ let GetModularBranch prog comp meth hInst =
| _ -> acc
) expr Set.empty
argSet |> Set.toList
+
+ let rec __UnifyImplies lhs rhs unifs =
+ let ___AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)
+
+ if lhs = FalseLiteral || rhs = TrueLiteral then
+ Some(unifs)
+ else
+ try
+ match lhs, rhs with
+ | VarLiteral(vname), rhs -> ___AddOrNone unifs vname rhs
+ | IntLiteral(nL), IntLiteral(nR) when nL = nR ->
+ Some(unifs)
+ | BoolLiteral(bL), BoolLiteral(bR) when bL = bR ->
+ Some(unifs)
+ | SetExpr(elistL), SetExpr(elistR)
+ | SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR ->
+ let unifs2 = List.fold2 (fun acc elL elR -> match __UnifyImplies elL elR acc with
+ | Some(u) -> u
+ | None -> raise CannotUnify) unifs elistL elistR
+ Some(unifs2)
+ | _ when lhs = rhs ->
+ Some(unifs)
+ | _ ->
+
+ let rec ___f2 target candidate unifs =
+ match target, candidate with
+ | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opT = opC ->
+ let builder = new CascadingBuilder<_>(None)
+ builder {
+ let! unifsLhs = __UnifyImplies lhsC lhsT unifs
+ let! unifsRhs = __UnifyImplies rhsC rhsT unifsLhs
+ return Some(unifsRhs)
+ }
+ | _ -> None
+
+ let rec ___f1 rhsLst lhsLst unifs =
+ match rhsLst, lhsLst with
+ | targetExpr :: rhsRest, candExpr :: lhsRest ->
+ // trying to find a unification for "targetExpr"
+ let uOpt = match ___f2 targetExpr candExpr unifs with
+ // found -> just return
+ | Some(unifs2) -> Some(unifs2)
+ // not found -> keep looking in the rest of the candidate expressions
+ | None -> ___f1 [targetExpr] lhsRest unifs
+ match uOpt with
+ // found -> try find for the rest of the target expressions
+ | Some(unifs2) -> ___f1 rhsRest lhsLst unifs2
+ // not found -> fail
+ | None -> None
+ | targetExpr :: _, [] ->
+ // no more candidates for unification for this targetExpr -> fail
+ None
+ | [], _ ->
+ // we've found unifications for all target expressions -> return the current unifications map
+ Some(unifs)
+
+// let candExprs = lhsLst |> List.choose (function BinaryExpr(_,cop,cl,cr) as e when cop = top -> Some(e) | _ -> None)
+// candExprs |> List.fold (fun acc candExpr ->
+// match candExpr with
+// | BinaryExpr(_,_,cl,cr) ->
+
+// let rec ___f1 lhsLst rhsLst unifs =
+// match rhsLst with
+// | targetExpr :: rhsRest ->
+// match targetExpr with
+// | BinaryExpr(_,"=",l,SequenceExpr(_)) ->
+// // this one has already been desugared so it's ok to skip it
+// ___f1 lhsLst rhsRest unifs
+// | BinaryExpr(_,top,tl,tr) ->
+// let candExprs = lhsLst |> List.choose (function BinaryExpr(_,cop,cl,cr) when cop = top -> Some(cr) | _ -> None)
+// match candExprs with
+// | [] -> None
+// | cand :: _ ->
+// let unifs2Opt = __UnifyImplies cand tr unifs
+// match unifs2Opt with
+// | Some(unifs2) -> ___f1 lhsLst rhsRest unifs2
+// | None -> None
+// | _ -> None
+// | [] -> Some(unifs)
+ //-----------
+ let lhsConjs = lhs |> DesugarRemove |> SplitIntoConjunts
+ let rhsConjs = rhs |> DesugarRemove |> SplitIntoConjunts
+ ___f1 rhsConjs lhsConjs unifs
+ with
+ | KeyAlreadyExists
+ | CannotUnify -> None
+
+ let __TryUnify targetMthd candMethod =
+ let targetPre,targetPost = GetMethodPrePost targetMthd
+ let candPre,candPost = GetMethodPrePost candMethod
+ let builder = new CascadingBuilder<_>(None)
+ builder {
+ let! unifs1 = __UnifyImplies targetPre candPre Map.empty
+ let! unifs2 = __UnifyImplies candPost targetPost unifs1
+ return Some(unifs2)
+ }
+
+ let rec __TryFindAMatch targetMthd candidateMethods =
+ match candidateMethods with
+ | candMthd :: rest ->
+ match __TryUnify targetMthd candMthd with
+ | Some(unifs) -> Some(candMthd,unifs)
+ | None -> __TryFindAMatch targetMthd rest
+ | [] -> None
+
+ let __TryFindExisting comp targetMthd =
+ Logger.TraceLine "Trying"
+ match __TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with
+ | Some(m,unifs) -> m,unifs
+ | None ->
+ let argsExprs = GetMethodArgs targetMthd |> List.fold (fun acc (Var(name,_)) -> acc |> Map.add name (VarLiteral(name))) Map.empty
+ targetMthd,argsExprs
+
let rec __GetDelegateMethods objs acc =
match objs with
| ObjLiteral(name) as obj :: rest ->
let mName = sprintf "_synth_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name
- let pre = TrueLiteral
+ let pre,_ = GetMethodPrePost meth //TrueLiteral
let post = __GetSpecFor name
let ins = __GetArgsUsed (BinaryAnd pre post)
let sgn = Sig(ins, [])
let m = Method(mName, sgn, pre, post, true)
- __GetDelegateMethods rest (acc |> Map.add obj m)
+ let c = FindComponent prog (name |> __GetObjLitType |> GetTypeShortName) |> Utils.ExtractOption
+ let m',unifs = __TryFindExisting c m
+ let args = GetMethodArgs m' |> List.map (fun (Var(name,_)) -> Map.find name unifs)
+ __GetDelegateMethods rest (acc |> Map.add obj (c,m',args))
| _ :: rest -> failwith "internal error: expected to see only ObjLiterals"
| [] -> acc
- let __FindObj objName =
- try
- hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst
- with
- | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)
+
(* --- function body starts here --- *)
let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty
let initChildrenExprList = delegateMethods |> Map.toList
- |> List.map (fun (receiver, mthd) ->
+ |> List.map (fun (receiver, (cmp,mthd,args)) ->
let key = __FindObj (PrintExpr 0 receiver), Var("", None)
- let args = GetMethodArgs mthd |> List.map (fun (Var(name,_)) -> VarLiteral(name))
let e = MethodCall(receiver, GetMethodName mthd, args)
(key, e)
)
let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)
- let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver newMthd ->
+ let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->
let obj = __FindObj (PrintExpr 0 receiver)
match acc with
| accProg, accComp, accmList ->
@@ -444,6 +576,9 @@ let rec MakeModular indent prog comp m cond heapInst =
/// Returns a (heap,env,ctx) tuple
// ============================================================================
let rec AnalyzeConstructor indent prog comp m =
+ // TODO: first check maybe there's already a method with this spec
+
+
let idt = Indent indent
let methodName = GetMethodName m
let pre,post = GetMethodPrePost m
@@ -451,7 +586,7 @@ let rec AnalyzeConstructor indent prog comp m =
let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral) false
Logger.InfoLine (idt + "[*] Analyzing constructor")
Logger.InfoLine (idt + "------------------------------------------")
- Logger.InfoLine (PrintMethodSignFull (indent + 4) m)
+ Logger.InfoLine (PrintMethodSignFull (indent + 4) comp m)
Logger.InfoLine (idt + "------------------------------------------")
Logger.Info (idt + " - searching for an instance ...")
let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))
@@ -572,34 +707,46 @@ let GetMethodsToAnalyze prog =
///
/// Returns a map from (component * method) |--> Expr * HeapInstance
// ============================================================================
-let rec AnalyzeMethods prog members =
- let rec __AnalyzeConstructorDeep prog mList =
+let rec AnalyzeMethods prog members solutionsSoFar =
+ let __IsAlreadySolved c m solutionMap =
+ let existingKey = solutionMap |> Map.tryFindKey (fun (cc,mm) v -> CheckSameMethods (c,m) (cc,mm) && not (v = []))
+ match existingKey with
+ | Some(_) -> true
+ | None -> false
+
+ let rec __AnalyzeConstructorDeep prog mList solutionsSoFar =
match mList with
| (comp,mthd) :: rest ->
- let sol = AnalyzeConstructor 2 prog comp mthd
- let unsolved = sol |> Map.filter (fun (c,m) lst -> lst = []) |> Utils.MapKeys
- sol |> MergeSolutions (__AnalyzeConstructorDeep prog (rest@unsolved))
- | [] -> Map.empty
+ if not (__IsAlreadySolved comp mthd solutionsSoFar) then
+ let sol = AnalyzeConstructor 2 prog comp mthd
+ let unsolved = sol |> Map.filter (fun (c,m) lst -> lst = [] && not(__IsAlreadySolved c m solutionsSoFar)) |> Utils.MapKeys
+ let newSols = solutionsSoFar |> MergeSolutions sol
+ __AnalyzeConstructorDeep prog (rest@unsolved) newSols
+ else
+ __AnalyzeConstructorDeep prog rest solutionsSoFar
+ | [] -> solutionsSoFar
+
(* --- function body starts here --- *)
match members with
| (comp,m) :: rest ->
match m with
| Method(_,_,_,_,true) ->
- let sol = __AnalyzeConstructorDeep prog [comp,m]
+ let sol = __AnalyzeConstructorDeep prog [comp,m] solutionsSoFar
Logger.InfoLine ""
- AnalyzeMethods prog rest |> MergeSolutions sol
- | _ -> AnalyzeMethods prog rest
- | [] -> Map.empty
+ AnalyzeMethods prog rest sol
+ | _ -> AnalyzeMethods prog rest solutionsSoFar
+ | [] -> solutionsSoFar
let Analyze prog filename =
let rec __AddMethodsFromProg methods solutions =
match methods with
| (c,m) :: rest ->
- let exists = solutions |> Map.tryFindKey (fun (c1,m1) _ -> GetComponentName c = GetComponentName c1 && GetMethodName m = GetMethodName m1)
+ let exists = solutions |> Map.tryFindKey (fun (c1,m1) _ -> CheckSameMethods (c,m) (c1,m1))
match exists with
| Some(_) -> __AddMethodsFromProg rest solutions
| None -> __AddMethodsFromProg rest (solutions |> Map.add (c,m) [])
| [] -> solutions
+
/// Prints given solutions to a file
let __PrintSolution prog outFileName solutions =
use file = System.IO.File.CreateText(outFileName)
@@ -610,8 +757,9 @@ let Analyze prog filename =
let extSolutions = solutions //__AddMethodsFromProg allMethods solutions
let synthCode = PrintImplCode prog extSolutions Options.CONFIG.genRepr
fprintfn file "%s" synthCode
+
(* --- function body starts here --- *)
- let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
+ let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) Map.empty
let progName = System.IO.Path.GetFileNameWithoutExtension(filename)
let outFlatSolFileName = dafnySynthFileNameTemplate.Replace("###", progName)
Logger.InfoLine "Printing synthesized code"
diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 15c93047..641a7143 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -454,6 +454,15 @@ let GetFrameFields comp =
v
)
+// ==============================================
+/// Checks whether two given methods are the same.
+///
+/// Methods are the same if their names are the
+/// same and their components have the same name.
+// ==============================================
+let CheckSameMethods (c1,m1) (c2,m2) =
+ GetComponentName c1 = GetComponentName c2 && GetMethodName m1 = GetMethodName m2
+
////////////////////////
let AddReplaceMethod prog comp newMthd oldMethod =
@@ -750,60 +759,66 @@ let EvalSym resolverFunc expr =
/// Desugars a given expression so that all list constructors
/// are expanded into explicit assignments to indexed elements
// ==========================================================
-let rec Desugar expr =
- match expr with
- | IntLiteral(_)
- | BoolLiteral(_)
- | IdLiteral(_)
- | VarLiteral(_)
- | ObjLiteral(_)
- | Star
- | Dot(_)
- | SelectExpr(_)
- | SeqLength(_)
- | UpdateExpr(_)
- | SetExpr(_)
- | MethodCall(_)
- | SequenceExpr(_) -> expr
- // forall v :: v in {a1 a2 ... an} ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]
- // forall v :: v in [a1 a2 ... an] ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]
- | ForallExpr([Var(vn1,ty1)] as v, (BinaryExpr(_, "==>", BinaryExpr(_, "in", VarLiteral(vn2), rhsCol), sub) as ee)) when vn1 = vn2 ->
- match rhsCol with
- | SetExpr(elist)
- | SequenceExpr(elist) -> elist |> List.fold (fun acc e -> BinaryAnd acc (Desugar (Substitute (VarLiteral(vn2)) e sub))) TrueLiteral
- | _ -> ForallExpr(v, Desugar ee)
- | ForallExpr(v,e) -> ForallExpr(v, Desugar e)
- | UnaryExpr(op,e) -> UnaryExpr(op, Desugar e)
- | IteExpr(c,e1,e2) -> IteExpr(c, Desugar e1, Desugar e2)
- // lst = [a1 a2 ... an] ~~~> lst = [a1 a2 ... an] && lst[0] = a1 && lst[1] = a2 && ... && lst[n-1] = an
- | BinaryExpr(p,op,e1,e2) ->
- let be = BinaryExpr(p, op, Desugar e1, Desugar e2)
- try
- match op with
- | "=" ->
- match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with
- | SequenceExpr(l1), SequenceExpr(l2) ->
- let rec __fff lst1 lst2 cnt =
- match lst1, lst2 with
- | fs1 :: rest1, fs2 :: rest2 -> BinaryEq l1.[cnt] l2.[cnt] :: __fff rest1 rest2 (cnt+1)
- | [], [] -> []
- | _ -> failwith "Lists are of different sizes"
- __fff l1 l2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
- | e, SequenceExpr(elist)
- | SequenceExpr(elist), e ->
- let rec __fff lst cnt =
- match lst with
- | fs :: rest -> BinaryEq (SelectExpr(e, IntLiteral(cnt))) elist.[cnt] :: __fff rest (cnt+1)
- | [] -> []
- __fff elist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
- | _ -> be
- | _ -> be
- with
- | EvalFailed(_) as ex -> (* printfn "%O" (ex.StackTrace); *) be
+let MyDesugar expr removeOriginal =
+ let rec __Desugar expr =
+ match expr with
+ | IntLiteral(_)
+ | BoolLiteral(_)
+ | IdLiteral(_)
+ | VarLiteral(_)
+ | ObjLiteral(_)
+ | Star
+ | Dot(_)
+ | SelectExpr(_)
+ | SeqLength(_)
+ | UpdateExpr(_)
+ | SetExpr(_)
+ | MethodCall(_)
+ | SequenceExpr(_) -> expr
+ // forall v :: v in {a1 a2 ... an} ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]
+ // forall v :: v in [a1 a2 ... an] ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]
+ | ForallExpr([Var(vn1,ty1)] as v, (BinaryExpr(_, "==>", BinaryExpr(_, "in", VarLiteral(vn2), rhsCol), sub) as ee)) when vn1 = vn2 ->
+ match rhsCol with
+ | SetExpr(elist)
+ | SequenceExpr(elist) -> elist |> List.fold (fun acc e -> BinaryAnd acc (__Desugar (Substitute (VarLiteral(vn2)) e sub))) TrueLiteral
+ | _ -> ForallExpr(v, __Desugar ee)
+ | ForallExpr(v,e) -> ForallExpr(v, __Desugar e)
+ | UnaryExpr(op,e) -> UnaryExpr(op, __Desugar e)
+ | IteExpr(c,e1,e2) -> IteExpr(c, __Desugar e1, __Desugar e2)
+ // lst = [a1 a2 ... an] ~~~> lst = [a1 a2 ... an] && lst[0] = a1 && lst[1] = a2 && ... && lst[n-1] = an && |lst| = n
+ | BinaryExpr(p,op,e1,e2) ->
+ let be = BinaryExpr(p, op, __Desugar e1, __Desugar e2)
+ let fs = if removeOriginal then TrueLiteral else be
+ try
+ match op with
+ | "=" ->
+ match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with
+ | SequenceExpr(l1), SequenceExpr(l2) ->
+ let rec __fff lst1 lst2 cnt =
+ match lst1, lst2 with
+ | fs1 :: rest1, fs2 :: rest2 -> BinaryEq l1.[cnt] l2.[cnt] :: __fff rest1 rest2 (cnt+1)
+ | [], [] -> []
+ | _ -> failwith "Lists are of different sizes"
+ __fff l1 l2 0 |> List.fold (fun acc e -> BinaryAnd acc e) fs
+ | e, SequenceExpr(elist)
+ | SequenceExpr(elist), e ->
+ let rec __fff lst cnt =
+ match lst with
+ | fs :: rest -> BinaryEq (SelectExpr(e, IntLiteral(cnt))) elist.[cnt] :: __fff rest (cnt+1)
+ | [] -> [BinaryEq (SeqLength(e)) (IntLiteral(cnt))]
+ __fff elist 0 |> List.fold (fun acc e -> BinaryAnd acc e) fs
+ | _ -> be
+ | _ -> be
+ with
+ | EvalFailed(_) as ex -> (* printfn "%O" (ex.StackTrace); *) be
+ __Desugar expr
+
+let Desugar expr = MyDesugar expr false
+let DesugarRemove expr = MyDesugar expr true
let rec DesugarLst exprLst =
match exprLst with
- | expr :: rest -> Desugar expr :: DesugarLst rest
+ | expr :: rest -> Desugar expr :: DesugarLst rest
| [] -> []
let ChangeThisReceiver receiver expr =
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 28e6b931..69a597cc 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
<WarningLevel>3</WarningLevel>
<PlatformTarget>x86</PlatformTarget>
<DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
- <StartArguments>examples/Set.jen /method:Set.Double /genRepr /genMod</StartArguments>
+ <StartArguments>examples/Set.jen /method:Set.Singleton /genRepr /genMod</StartArguments>
<StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index ca65f495..6f9f9de5 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -129,18 +129,18 @@ let PrintDecl d =
| Code(id,typeParams) ->
(PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline
-let PrintMethodSignFull indent m =
+let PrintMethodSignFull indent comp m =
let idt = Indent indent
let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";")
+ let compName = GetComponentName comp
match m with
| Method(methodName, sgn, pre, post, isConstr) ->
let mc = if isConstr then "constructor" else "method"
let preStr = (__PrintPrePost (idt + " requires ") pre)
let postStr = (__PrintPrePost (idt + " ensures ") post)
- idt + mc + " " + methodName + (PrintSig sgn) + newline +
+ idt + mc + " " + compName + "." + methodName + (PrintSig sgn) + newline +
preStr + (if preStr = "" then "" else newline) +
- postStr
-
+ postStr
| _ -> failwithf "not a method: %O" m
let Print prog =
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index b6d10060..d5251a08 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -221,6 +221,23 @@ let rec ListSet idx v lst =
fs :: ListSet (idx-1) v rest
| [] -> failwith "index out of range"
+exception KeyAlreadyExists
+
+// =======================================
+/// requires (key |--> value) !in map
+///
+/// ensures ret = map ++ (key |--> value)
+// =======================================
+let MapAddNew key value map =
+ match Map.tryFind key map with
+ | Some(existingValue) ->
+ if existingValue = value then
+ map
+ else
+ raise KeyAlreadyExists
+ | None ->
+ map |> Map.add key value
+
// =======================================
/// ensures: forall k,v ::
/// if k,v in map2 then
diff --git a/Jennisys/Jennisys/examples/List2.jen b/Jennisys/Jennisys/examples/List2.jen
index 116804fa..acca4ddf 100644
--- a/Jennisys/Jennisys/examples/List2.jen
+++ b/Jennisys/Jennisys/examples/List2.jen
@@ -42,6 +42,12 @@ class IntNode {
constructor SingletonZero()
ensures list = [0]
+
+ constructor Init(x: int)
+ ensures list = [x]
+
+ constructor Double(x: int, y: int)
+ ensures list = [x y]
}
model IntNode {
diff --git a/Jennisys/Jennisys/examples/Set.jen b/Jennisys/Jennisys/examples/Set.jen
index 3bee04e8..60a294c1 100644
--- a/Jennisys/Jennisys/examples/Set.jen
+++ b/Jennisys/Jennisys/examples/Set.jen
@@ -11,6 +11,7 @@ class Set {
ensures elems = {p + q}
constructor Double(p: int, q: int)
+ requires p != q
ensures elems = {p q}
constructor Triple(p: int, q: int, r: int)
@@ -32,16 +33,20 @@ model Set {
class SetNode {
var elems: set[int]
- constructor Init(t: int)
- ensures elems = {t}
+ constructor Init(x: int)
+ ensures elems = {x}
- constructor Double(p: int, q: int)
- requires p != q
- ensures elems = {p q}
+ constructor Double(x: int, y: int)
+ requires x != y
+ ensures elems = {x y}
- constructor Triple(p: int, q: int, r: int)
- requires p != q && q != r && r != p
- ensures elems = {p q r}
+ constructor Double2(x: int, y: int)
+ requires x > y
+ ensures elems = {x y}
+
+ constructor Triple(x: int, y: int, z: int)
+ requires x != y && y != z && z != x
+ ensures elems = {x y z}
}
model SetNode {
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy
new file mode 100644
index 00000000..e3f7a701
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy
@@ -0,0 +1,139 @@
+class List<T> {
+ ghost var Repr: set<object>;
+ ghost var list: seq<T>;
+
+ var root: Node<T>;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (root == null ==> |list| == 0) &&
+ (root != null ==> list == root.list)
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (root != null ==> root.Valid())
+ }
+
+
+ method Double(p: T, q: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p, q];
+ {
+ var gensym68 := new Node<T>;
+ gensym68.Double(p, q);
+ this.list := [p, q];
+ this.root := gensym68;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Empty()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [];
+ {
+ this.list := [];
+ this.root := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Singleton(t: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [t];
+ {
+ var gensym67 := new Node<T>;
+ gensym67.Init(t);
+ this.list := [t];
+ this.root := gensym67;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+}
+
+class Node<T> {
+ ghost var Repr: set<object>;
+ ghost var list: seq<T>;
+
+ var data: T;
+ var next: Node<T>;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (next == null <==> (list == [data] && list[0] == data) && |list| == 1) &&
+ (next != null ==> list == [data] + next.list) &&
+ (|list| > 0)
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (next != null ==> next.Valid_self()) &&
+ (next != null && next.next != null ==> next.next.Valid_self())
+ }
+
+
+ method Double(p: T, q: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p, q];
+ {
+ var gensym74 := new Node<T>;
+ gensym74.Init(q);
+ this.data := p;
+ this.list := [p, q];
+ this.next := gensym74;
+ // repr stuff
+ this.Repr := {this} + this.next.Repr;
+ }
+
+
+ method Init(t: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [t];
+ {
+ this.data := t;
+ this.list := [t];
+ this.next := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy
new file mode 100644
index 00000000..08268640
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy
@@ -0,0 +1,213 @@
+class IntList {
+ ghost var Repr: set<object>;
+ ghost var list: seq<int>;
+
+ var root: IntNode;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (root == null <==> |list| == 0) &&
+ (root != null ==> list == root.list)
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (root != null ==> root.Valid())
+ }
+
+
+ method Double(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p] + [q];
+ {
+ var gensym67 := new IntNode;
+ gensym67.Double(p, q);
+ this.list := [p] + [q];
+ this.root := gensym67;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Empty()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [];
+ {
+ this.list := [];
+ this.root := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method OneTwo()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [1, 2];
+ {
+ var gensym65 := new IntNode;
+ gensym65.Double(1, 2);
+ this.list := [1, 2];
+ this.root := gensym65;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Singleton(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p];
+ {
+ var gensym66 := new IntNode;
+ gensym66.Init(p);
+ this.list := [p];
+ this.root := gensym66;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method SingletonTwo()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [2];
+ {
+ var gensym65 := new IntNode;
+ gensym65.Init(2);
+ this.list := [2];
+ this.root := gensym65;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Sum(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p + q];
+ {
+ var gensym67 := new IntNode;
+ gensym67.Init(p + q);
+ this.list := [p + q];
+ this.root := gensym67;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method TwoConsecutive(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p] + [p + 1];
+ {
+ var gensym66 := new IntNode;
+ gensym66.Double(p, p + 1);
+ this.list := [p] + [p + 1];
+ this.root := gensym66;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+}
+
+class IntNode {
+ ghost var Repr: set<object>;
+ ghost var list: seq<int>;
+
+ var data: int;
+ var next: IntNode;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&
+ (next != null ==> list == [data] + next.list) &&
+ (|list| > 0)
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (next != null ==> next.Valid_self()) &&
+ (next != null && next.next != null ==> next.next.Valid_self())
+ }
+
+
+ method SingletonZero()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [0];
+ {
+ this.data := 0;
+ this.list := [0];
+ this.next := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Double(x: int, y: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [x, y];
+ {
+ var gensym74 := new IntNode;
+ gensym74.Init(y);
+ this.data := x;
+ this.list := [x, y];
+ this.next := gensym74;
+ // repr stuff
+ this.Repr := {this} + this.next.Repr;
+ }
+
+
+ method Init(x: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [x];
+ {
+ this.data := x;
+ this.list := [x];
+ this.next := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy
new file mode 100644
index 00000000..9eba9fe6
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy
@@ -0,0 +1,393 @@
+class IntList {
+ ghost var Repr: set<object>;
+ ghost var list: seq<int>;
+
+ var root: IntNode;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (root == null ==> |list| == 0) &&
+ (root != null ==> |list| == |root.succ| + 1 && (list[0] == root.data && (forall i :: 1 <= i && i <= |root.succ| ==> root.succ[i - 1] != null && list[i] == root.succ[i - 1].data)))
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (root != null ==> root.Valid())
+ }
+
+
+ method Double(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p] + [q];
+ {
+ var gensym68 := new IntNode;
+ gensym68._synth_IntList_Double_gensym68(p, q);
+ this.list := [p] + [q];
+ this.root := gensym68;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Empty()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [];
+ {
+ this.list := [];
+ this.root := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method OneTwo()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [1, 2];
+ {
+ var gensym65 := new IntNode;
+ gensym65._synth_IntList_OneTwo_gensym65();
+ this.list := [1, 2];
+ this.root := gensym65;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Singleton(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p];
+ {
+ var gensym67 := new IntNode;
+ gensym67._synth_IntList_Singleton_gensym67(p);
+ this.list := [p];
+ this.root := gensym67;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method SingletonTwo()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [2];
+ {
+ var gensym66 := new IntNode;
+ gensym66._synth_IntList_SingletonTwo_gensym66();
+ this.list := [2];
+ this.root := gensym66;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Sum(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p + q];
+ {
+ var gensym68 := new IntNode;
+ gensym68._synth_IntList_Sum_gensym68(p, q);
+ this.list := [p + q];
+ this.root := gensym68;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method TwoConsecutive(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p] + [p + 1];
+ {
+ var gensym67 := new IntNode;
+ gensym67._synth_IntList_TwoConsecutive_gensym67(p);
+ this.list := [p] + [p + 1];
+ this.root := gensym67;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+}
+
+class IntNode {
+ ghost var Repr: set<object>;
+ ghost var succ: seq<IntNode>;
+ ghost var data: int;
+
+ var next: IntNode;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (next == null ==> |succ| == 0) &&
+ (next != null ==> succ == [next] + next.succ) &&
+ (!(null in succ))
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (next != null ==> next.Valid_self()) &&
+ (next != null && next.next != null ==> next.next.Valid_self())
+ }
+
+
+ method Init(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == p;
+ {
+ this.data := p;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method InitInc(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == p + 1;
+ {
+ this.data := p + 1;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Zero()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == 0;
+ ensures succ == [];
+ {
+ this.data := 0;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method _synth_IntList_Double_gensym68(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == p;
+ ensures |succ| == 1;
+ ensures succ[0].data == q;
+ ensures succ[0].succ == [];
+ {
+ var gensym80 := new IntNode;
+ gensym80._synth_IntNode__synth_IntList_Double_gensym68_gensym80(q);
+ this.data := p;
+ this.next := gensym80;
+ this.succ := [gensym80];
+ // repr stuff
+ this.Repr := {this} + this.next.Repr;
+ }
+
+
+ method _synth_IntList_OneTwo_gensym65()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == 1;
+ ensures |succ| == 1;
+ ensures succ[0].data == 2;
+ ensures succ[0].succ == [];
+ {
+ var gensym78 := new IntNode;
+ gensym78._synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78();
+ this.data := 1;
+ this.next := gensym78;
+ this.succ := [gensym78];
+ // repr stuff
+ this.Repr := {this} + this.next.Repr;
+ }
+
+
+ method _synth_IntList_SingletonTwo_gensym66()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == 2;
+ ensures |succ| == 0;
+ {
+ this.data := 2;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method _synth_IntList_Singleton_gensym67(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == p;
+ ensures |succ| == 0;
+ {
+ this.data := p;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method _synth_IntList_Sum_gensym68(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == p + q;
+ ensures |succ| == 0;
+ {
+ this.data := p + q;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method _synth_IntList_TwoConsecutive_gensym67(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == p;
+ ensures |succ| == 1;
+ ensures succ[0].data == p + 1;
+ ensures succ[0].succ == [];
+ {
+ var gensym79 := new IntNode;
+ gensym79._synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p);
+ this.data := p;
+ this.next := gensym79;
+ this.succ := [gensym79];
+ // repr stuff
+ this.Repr := {this} + this.next.Repr;
+ }
+
+
+ method OneTwo()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == 1;
+ ensures |succ| == 1;
+ ensures succ[0] != null;
+ ensures succ[0].data == 2;
+ {
+ var gensym73 := new IntNode;
+ gensym73._synth_IntNode_OneTwo_gensym73();
+ this.data := 1;
+ this.next := gensym73;
+ this.succ := [gensym73];
+ // repr stuff
+ this.Repr := {this} + this.next.Repr;
+ }
+
+
+ method _synth_IntNode_OneTwo_gensym73()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == 2;
+ ensures |succ| == 0;
+ {
+ this.data := 2;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method _synth_IntNode__synth_IntList_Double_gensym68_gensym80(q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == q;
+ ensures |succ| == 0;
+ {
+ this.data := q;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method _synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == 2;
+ ensures |succ| == 0;
+ {
+ this.data := 2;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method _synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures data == p + 1;
+ ensures |succ| == 0;
+ {
+ this.data := p + 1;
+ this.next := null;
+ this.succ := [];
+ // repr stuff
+ this.Repr := {this};
+ }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
new file mode 100644
index 00000000..3f1e6b4b
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
@@ -0,0 +1,233 @@
+class Number {
+ ghost var Repr: set<object>;
+ ghost var num: int;
+
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ true
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ true
+ }
+
+
+ method Double(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num == 2 * p;
+ {
+ this.num := 2 * p;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Init(p: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num == p;
+ {
+ this.num := p;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Sum(a: int, b: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num == a + b;
+ {
+ this.num := a + b;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Abs(a: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num in {a, -a};
+ ensures num >= 0;
+ {
+ if (a >= 0) {
+ this.num := a;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ this.num := -a;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+
+
+ method Min4(a: int, b: int, c: int, d: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num in {a, b, c, d};
+ ensures (forall x :: x in {a, b, c, d} ==> num <= x);
+ {
+ if (a <= b && (a <= c && a <= d)) {
+ this.num := a;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ if (d <= a && (d <= b && d <= c)) {
+ this.num := d;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ if (c <= a && (c <= b && c <= d)) {
+ this.num := c;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ this.num := b;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+ }
+ }
+
+
+ method MinSum(a: int, b: int, c: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num in {a + b, a + c, b + c};
+ ensures num <= a + b;
+ ensures num <= b + c;
+ ensures num <= a + c;
+ {
+ if (a + b <= b + c && a + b <= a + c) {
+ this.num := a + b;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ if (a + c <= a + b && a + c <= b + c) {
+ this.num := a + c;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ this.num := b + c;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+ }
+
+
+ method Min32(a: int, b: int, c: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num in {a, b, c};
+ ensures (forall x :: x in {a, b, c} ==> num <= x);
+ {
+ if (a <= b && a <= c) {
+ this.num := a;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ if (c <= a && c <= b) {
+ this.num := c;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ this.num := b;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+ }
+
+
+ method Min3(a: int, b: int, c: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num in {a, b, c};
+ ensures num <= a;
+ ensures num <= b;
+ ensures num <= c;
+ {
+ if (a <= b && a <= c) {
+ this.num := a;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ if (c <= a && c <= b) {
+ this.num := c;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ this.num := b;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+ }
+
+
+ method Min22(a: int, b: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures num in {a, b};
+ ensures num <= a;
+ ensures num <= b;
+ {
+ if (a <= b) {
+ this.num := a;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ this.num := b;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+
+
+ method Min2(a: int, b: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures a < b ==> num == a;
+ ensures a >= b ==> num == b;
+ {
+ if (a >= b ==> a == b) {
+ this.num := a;
+ // repr stuff
+ this.Repr := {this};
+ } else {
+ this.num := b;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
new file mode 100644
index 00000000..f754d540
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
@@ -0,0 +1,269 @@
+class Set {
+ ghost var Repr: set<object>;
+ ghost var elems: set<int>;
+
+ var root: SetNode;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (root == null ==> elems == {}) &&
+ (root != null ==> elems == root.elems)
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (root != null ==> root.Valid())
+ }
+
+
+ method Double(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {p, q};
+ {
+ var gensym67 := new SetNode;
+ gensym67.Double(p, q);
+ this.elems := {p, q};
+ this.root := gensym67;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Empty()
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {};
+ {
+ this.elems := {};
+ this.root := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Singleton(t: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {t};
+ {
+ var gensym67 := new SetNode;
+ gensym67.Init(t);
+ this.elems := {t};
+ this.root := gensym67;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+
+ method Sum(p: int, q: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {p + q};
+ {
+ var gensym69 := new SetNode;
+ gensym69.Init(p + q);
+ this.elems := {p + q};
+ this.root := gensym69;
+ // repr stuff
+ this.Repr := {this} + this.root.Repr;
+ }
+
+}
+
+class SetNode {
+ ghost var Repr: set<object>;
+ ghost var elems: set<int>;
+
+ var data: int;
+ var left: SetNode;
+ var right: SetNode;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&
+ (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&
+ (left != null ==> (forall e :: e in left.elems ==> e < data)) &&
+ (right != null ==> (forall e :: e in right.elems ==> e > data))
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ (left != null ==> left.Valid_self()) &&
+ (right != null ==> right.Valid_self()) &&
+ (left != null && left.left != null ==> left.left.Valid_self()) &&
+ (left != null && left.right != null ==> left.right.Valid_self()) &&
+ (right != null && right.left != null ==> right.left.Valid_self()) &&
+ (right != null && right.right != null ==> right.right.Valid_self())
+ }
+
+
+ method Init(x: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {x};
+ {
+ this.data := x;
+ this.elems := {x};
+ this.left := null;
+ this.right := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Triple(x: int, y: int, z: int)
+ modifies this;
+ requires x != y;
+ requires y != z;
+ requires z != x;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {x, y, z};
+ {
+ if (x < y && z > y) {
+ var gensym80 := new SetNode;
+ var gensym81 := new SetNode;
+ gensym80.Init(z);
+ gensym81.Init(x);
+ this.data := y;
+ this.elems := {x, y, z};
+ this.left := gensym81;
+ this.right := gensym80;
+ // repr stuff
+ this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+ } else {
+ if (z < x && y > x) {
+ var gensym80 := new SetNode;
+ var gensym81 := new SetNode;
+ gensym80.Init(y);
+ gensym81.Init(z);
+ this.data := x;
+ this.elems := {x, y, z};
+ this.left := gensym81;
+ this.right := gensym80;
+ // repr stuff
+ this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+ } else {
+ if (x < z && y > z) {
+ var gensym80 := new SetNode;
+ var gensym81 := new SetNode;
+ gensym80.Init(y);
+ gensym81.Init(x);
+ this.data := z;
+ this.elems := {x, y, z};
+ this.left := gensym81;
+ this.right := gensym80;
+ // repr stuff
+ this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+ } else {
+ if (z < y && x > y) {
+ var gensym80 := new SetNode;
+ var gensym81 := new SetNode;
+ gensym80.Init(x);
+ gensym81.Init(z);
+ this.data := y;
+ this.elems := {x, y, z};
+ this.left := gensym81;
+ this.right := gensym80;
+ // repr stuff
+ this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+ } else {
+ if (y < z && x > z) {
+ var gensym80 := new SetNode;
+ var gensym81 := new SetNode;
+ gensym80.Init(x);
+ gensym81.Init(y);
+ this.data := z;
+ this.elems := {x, y, z};
+ this.left := gensym81;
+ this.right := gensym80;
+ // repr stuff
+ this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+ } else {
+ var gensym80 := new SetNode;
+ var gensym81 := new SetNode;
+ gensym80.Init(z);
+ gensym81.Init(y);
+ this.data := x;
+ this.elems := {x, y, z};
+ this.left := gensym81;
+ this.right := gensym80;
+ // repr stuff
+ this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+ }
+ }
+ }
+ }
+ }
+ }
+
+
+ method Double(x: int, y: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {x, y};
+ {
+ if (y > x) {
+ var gensym77 := new SetNode;
+ gensym77.Init(y);
+ this.data := x;
+ this.elems := {x, y};
+ this.left := null;
+ this.right := gensym77;
+ // repr stuff
+ this.Repr := {this} + this.right.Repr;
+ } else {
+ if (x > y) {
+ var gensym77 := new SetNode;
+ gensym77.Init(x);
+ this.data := y;
+ this.elems := {x, y};
+ this.left := null;
+ this.right := gensym77;
+ // repr stuff
+ this.Repr := {this} + this.right.Repr;
+ } else {
+ this.data := y;
+ this.elems := {x, y};
+ this.left := null;
+ this.right := null;
+ // repr stuff
+ this.Repr := {this};
+ }
+ }
+ }
+
+}
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 11:49:25 +0000