diff options
| author |  Rustan Leino <unknown> | 2013-07-29 14:51:40 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-29 14:51:40 -0700 |
| commit | 0fec0bd429d2333d64c13a015d4e34525a3f65a5 (patch) | |
| tree | 13cd0cf68c2df16bb654462d23a88586763ae887 /Test/vstte2012 | |
| parent | 5b6f3990bbad75baf5fcd7343dfc586bb93522db (diff) | |
Added an assert to help the theorem prover out in the RingBuffer.Enqueue method.
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/RingBuffer.dfy | 2 | ||||
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Test/vstte2012/RingBuffer.dfy b/Test/vstte2012/RingBuffer.dfy index 35e95165..e943b68d 100644 --- a/Test/vstte2012/RingBuffer.dfy +++ b/Test/vstte2012/RingBuffer.dfy @@ -74,7 +74,7 @@ class RingBuffer<T> ensures Valid() && fresh(Repr - old(Repr));
ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);
{
- x := data[start];
+ x := data[start]; assert x == Contents[0];
start, len := if start + 1 == data.Length then 0 else start + 1, len - 1;
Contents := Contents[1..];
}
diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy index 7ce48fcc..aa7f171a 100644 --- a/Test/vstte2012/RingBufferAuto.dfy +++ b/Test/vstte2012/RingBufferAuto.dfy @@ -59,7 +59,7 @@ class {:autocontracts} RingBuffer<T> ensures Valid() && fresh(Repr - old(Repr));
ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);
{
- x := data[start];
+ x := data[start]; assert x == Contents[0];
start, len := if start + 1 == data.Length then 0 else start + 1, len - 1;
Contents := Contents[1..];
}
|