diff options
| author |  rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
| commit | ea1898f88e2edcecf3a58923fcd1a5d2b87219a8 (patch) | |
| tree | 82944147dd136bf68b4cb2f8e40d440c6705d42e /Source/Forro/BoogieAst.fs | |
| parent | 8d1dd0f01a78bf29aa98832317d8fc951ed15075 (diff) | |
Introducing Forr?! Forr? is a tiny language that translates to Boogie. The purpose of the language and verifier is to serve as a tutorial example for how to build a verifier on top of Boogie.
Diffstat (limited to 'Source/Forro/BoogieAst.fs')
| -rw-r--r-- | Source/Forro/BoogieAst.fs | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/Source/Forro/BoogieAst.fs b/Source/Forro/BoogieAst.fs new file mode 100644 index 00000000..964f6667 --- /dev/null +++ b/Source/Forro/BoogieAst.fs @@ -0,0 +1,40 @@ +namespace BoogieAst
+
+type BType = BInt | BBool
+
+type BOperator = BEq | BNeq | BPlus | BMinus | BTimes | BLess | BAtMost | BAnd | BOr
+
+type BExpression =
+ | BConstant of int
+ | BFalse
+ | BTrue
+ | BNull
+ | BIdentifier of string
+ | BNot of BExpression
+ | BBinary of BOperator * BExpression * BExpression
+ | BSelect of string * BExpression
+ | BToPred of BExpression // BToPred(e) == (e != 0)
+ | BToTerm of BExpression // BToTerm(e) == (if e then 1 else 0)
+ | BOld of BExpression
+ | BFunc of string * BExpression list
+
+type BStmtList =
+ BBlock of Statement list
+
+and Statement =
+ | BAssign of string * BExpression
+ | BUpdate of string * BExpression * BExpression
+ | BHavoc of string list
+ | BAssert of BExpression
+ | BAssume of BExpression
+ | BIfStmt of BExpression * BStmtList * BStmtList
+ | BWhileStmt of BExpression * BExpression list * BStmtList
+ | BCallStmt of string list * string * BExpression list
+
+type BVarDecl = BVar of string * BType
+
+type BProcedure =
+ BProc of string * BVarDecl list * BVarDecl list * BExpression * string list * BExpression * BVarDecl list * BStmtList
+
+type BProgram =
+ BProg of string * BProcedure list
|