diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-10-05 19:11:23 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-10-05 19:11:23 -0700 |
| commit | 696796e1dcea137ee9b5c270b233892dd3267155 (patch) | |
| tree | d7886f80fd90265c688585c6a05508d860078381 /Test/datatypes | |
| parent | f878eae7ec3b85cc6b66040def0993c8bcc1e28c (diff) | |
implementing datatypes
Diffstat (limited to 'Test/datatypes')
| -rw-r--r-- | Test/datatypes/t1.bpl | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl new file mode 100644 index 00000000..61409465 --- /dev/null +++ b/Test/datatypes/t1.bpl @@ -0,0 +1,20 @@ +type TT;
+type {:datatype} Tree;
+function {:constructor} leaf() : Tree;
+function {:constructor} node(value:TT, children:TreeList) : Tree;
+
+type {:datatype} TreeList;
+function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;
+function {:constructor} nil() : TreeList;
+
+procedure foo()
+{
+ var a: Tree;
+ var b: TreeList;
+ var x: TT;
+
+ assert value#node(node(x, nil())) == x;
+ assert children#node(node(x, nil())) == nil();
+
+ assert (cons(leaf(), nil()) == nil());
+}
\ No newline at end of file |