From 0fec0bd429d2333d64c13a015d4e34525a3f65a5 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 29 Jul 2013 14:51:40 -0700 Subject: Added an assert to help the theorem prover out in the RingBuffer.Enqueue method. --- Test/vstte2012/RingBuffer.dfy | 2 +- Test/vstte2012/RingBufferAuto.dfy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/vstte2012') 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 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 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..]; } -- cgit v1.2.3