diff options
| author |  Rustan Leino <unknown> | 2014-07-08 13:47:08 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-08 13:47:08 -0700 |
| commit | 2c93b838927128721698eba02c146af4e716ce4d (patch) | |
| tree | b84125a88f46f6b5a4cbc1323153b33c5b6ca8a0 /Test/vstte2012 | |
| parent | 1844457f6a4a51592103c67de5f67a8785d8c92f (diff) | |
Cleaned up a test program
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy index a4bdf0a0..142d0279 100644 --- a/Test/vstte2012/RingBufferAuto.dfy +++ b/Test/vstte2012/RingBufferAuto.dfy @@ -76,8 +76,6 @@ class {:autocontracts} RingBuffer<T> method Dequeue() returns (x: T)
requires Contents != [];
- modifies Repr;
- ensures Valid() && fresh(Repr - old(Repr));
ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);
{
x := data[start]; assert x == Contents[0];
|