diff options
| author |  rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
| commit | 2efa59dea051803bc716d02070aa013397cfccc4 (patch) | |
| tree | bea0fe3564ee6b336db622f8c24a13552f68d10d /Test/VSI-Benchmarks | |
| parent | 61993a0cf682448770a0e3223ba560171635c3af (diff) | |
Added a sequence update expression in Dafny.
Diffstat (limited to 'Test/VSI-Benchmarks')
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 2 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 4 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 4 |
3 files changed, 3 insertions, 7 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 4f44612d..ed121ba0 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -100,7 +100,7 @@ class Benchmark3 { call r.Enqueue(m);
pperm:= pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] +[pperm[k]];
}
- assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //needed to trigger axiom
+ assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index e3a99884..3fa80b4c 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -52,10 +52,8 @@ class Map<Key,Value> { if (j == -1) {
keys := keys + [key];
values := values + [val];
- assert values[|keys|-1] == val; // lemma
} else {
- values := values[..j] + [val] + values[j+1..];
- assert values[j] == val; //lemma
+ values := values[j := val];
}
}
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index c3374605..bc26ee85 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -298,10 +298,8 @@ class Map<Key,Value> { if (j == -1) {
keys := keys + [key];
values := values + [val];
- assert values[|keys|-1] == val; // lemma
} else {
- values := values[..j] + [val] + values[j+1..];
- assert values[j] == val; //lemma
+ values := values[j := val];
}
}
|