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/Ast.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/Ast.fs')
| -rw-r--r-- | Source/Forro/Ast.fs | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/Source/Forro/Ast.fs b/Source/Forro/Ast.fs new file mode 100644 index 00000000..fa4db8ec --- /dev/null +++ b/Source/Forro/Ast.fs @@ -0,0 +1,34 @@ +namespace Forro
+
+type Field = Head | Tail | Valid
+
+type Variable = Var of string
+
+type Operator = Eq | Neq | Plus | Minus | Times | Less | AtMost | And | Or
+
+type Expression =
+ | Constant of int
+ | Null
+ | Identifier of Variable
+ | Not of Expression
+ | Binary of Operator * Expression * Expression
+ | Select of Expression * Field
+ | Old of Expression
+
+type StmtList =
+ Block of Statement list
+
+and Statement =
+ | Assign of Variable * Expression
+ | Update of Expression * Field * Expression
+ | Alloc of Variable * Expression * Expression
+ | IfStmt of Expression * StmtList * StmtList
+ | WhileStmt of Expression * Expression list * StmtList
+ | CallStmt of Variable list * string * Expression list
+ | Assert of Expression
+
+type Procedure =
+ Proc of string * Variable list * Variable list * Expression * Expression * StmtList
+
+type Program =
+ Prog of Procedure list
|