From 9b8c0b44fc7ffa9d292b46d63965a2431c19e2ae Mon Sep 17 00:00:00 2001 From: Unknown Date: Sun, 3 Jul 2011 17:59:13 -0700 Subject: added some doc comments --- Jennisys/Analyzer.fs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'Jennisys/Analyzer.fs') diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index fab61ff4..48adcca1 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -43,15 +43,12 @@ let GenMethodAnalysisCode comp methodName signature pre post = (match signature with | Sig(ins,outs) -> List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "") + - // assume preconditions " // assume precondition" + newline + " assume " + (PrintExpr 0 pre) + ";" + newline + - // assume invariant and postcondition " // assume invariant and postcondition" + newline + " assume Valid();" + newline + " assume " + (PrintExpr 0 post) + ";" + newline + - // inline the user defined invariant because assuming Valid() doesn't always work - " // assume user defined invariant again because assuming Valid() doesn't always work" + + " // assume user defined invariant again because assuming Valid() doesn't always work" + newline + (GetInvariantsAsList comp |> PrintSep newline (fun e -> " assume " + (PrintExpr 0 e) + ";")) + newline + // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible " // assert false to search for a model satisfying the assumed constraints" + newline + @@ -66,6 +63,7 @@ let MethodAnalysisPrinter onlyForThisCompMethod comp mthd = | _ -> "" | _ -> "" +/// Returns whether the code synthesized for the given method can be verified with Dafny let VerifySolution (heap,env,ctx) prog comp mthd = // print the solution to file and try to verify it with Dafny let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx) -- cgit v1.2.3