diff options
| author |  Unknown <t-alekm@A3479878.redmond.corp.microsoft.com> | 2011-07-02 18:29:27 -0700 |
|---|---|---|
| committer | Unknown <t-alekm@A3479878.redmond.corp.microsoft.com> | 2011-07-02 18:29:27 -0700 |
| commit | 8a7d7782f7f13f60e8638b3988b9d12d33ffa571 (patch) | |
| tree | b99629d903f5e1b48a1f8426e303a5a3f6d25984 /Jennisys/Ast.fs | |
| parent | fdddb2f9d1038a605fba4153242714f066e29aff (diff) | |
- when analyzing a constructor, repeated "assume <inv>" statement explicitly
since "assume Valid()" doesn't always work
- added optional verification step after code has been synthesized
Diffstat (limited to 'Jennisys/Ast.fs')
| -rw-r--r-- | Jennisys/Ast.fs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs index 45fd2aff..26d27fef 100644 --- a/Jennisys/Ast.fs +++ b/Jennisys/Ast.fs @@ -51,7 +51,7 @@ type Member = type TopLevelDecl =
| Class of string * string list * Member list
- | Model of string * string list * VarDecl list * Expr list * Expr
+ | Model of string * string list * VarDecl list * (* frame *) Expr list * (* invariant *) Expr
| Code of string * string list
type SyntacticProgram =
|