diff options
| author |  Rustan Leino <unknown> | 2013-08-04 17:55:06 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-04 17:55:06 -0700 |
| commit | a1710a324a8d92935cd7bc8ecbda115b9cd09748 (patch) | |
| tree | 0da87df5c79764cc7d46da695561ea8134f60146 /Test/dafny0/StatementExpressions.dfy | |
| parent | 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 (diff) | |
Set up call-graph to keep track of edges between functions and methods. (To be done: replace InMethodContext with a Function/Method-Height in translator.)
Diffstat (limited to 'Test/dafny0/StatementExpressions.dfy')
| -rw-r--r-- | Test/dafny0/StatementExpressions.dfy | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/Test/dafny0/StatementExpressions.dfy b/Test/dafny0/StatementExpressions.dfy new file mode 100644 index 00000000..9f33b282 --- /dev/null +++ b/Test/dafny0/StatementExpressions.dfy @@ -0,0 +1,58 @@ +ghost method M(n: nat) //returns (y: nat)
+{
+ var y := F(n, 0);
+}
+function F(n: nat, p: int): nat
+{
+ calc {
+ 100;
+ < { if n != 0 { M(n-1); } }
+ 102;
+ }
+ n
+}
+
+ghost method MM(n: nat) returns (y: nat)
+ decreases n, 0;
+{
+ if n != 0 {
+ y := FF(n-1);
+ }
+}
+function FF(n: nat): nat
+ decreases n, 1;
+{
+ calc {
+ 100;
+ < { var y := MM(n); }
+ 102;
+ }
+ n
+}
+
+ghost method P(n: nat)
+{
+ if n != 0 {
+ var y :=
+ calc {
+ 12;
+ { P(n-1); }
+ 12;
+ }
+ 100;
+ assert y == 100;
+ }
+}
+ghost method Q(n: nat)
+{
+ if n != 0 {
+ var y :=
+ calc {
+ 12;
+ { Q(n+1); } // error: cannot prove termination
+ 12;
+ }
+ 100;
+ assert y == 102; // error: assertion does not hold
+ }
+}
|