diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
| commit | d9f2a82a417703f3669ba8399dcc8bcf34c3d742 (patch) | |
| tree | 08b309fd809639a62c453c33dac86845dd4b9815 /Test/vacid0/SparseArray.dfy | |
| parent | e52270deab6d2fd5b885848211c2d9d1ab814b09 (diff) | |
Dafny: retired the "call" keyword
Diffstat (limited to 'Test/vacid0/SparseArray.dfy')
| -rw-r--r-- | Test/vacid0/SparseArray.dfy | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index 2c217264..989ddfc6 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -37,11 +37,9 @@ class SparseArray<T> { ensures |Contents| == N && this.zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
- var aa;
- var ii;
- call aa := AllocateArray(N); this.a := aa;
- call ii := AllocateArray(N); this.b := ii;
- call ii := AllocateArray(N); this.c := ii;
+ var aa := AllocateArray(N); this.a := aa;
+ var bb := AllocateArray(N); this.b := bb;
+ bb := AllocateArray(N); this.c := bb;
this.n := 0;
// initialize ghost variable Contents to a sequence of length N containing only zero's,
|