diff options
| author |  Unknown <namin@idea> | 2013-06-26 17:48:12 -0700 |
|---|---|---|
| committer | Unknown <namin@idea> | 2013-06-26 17:48:12 -0700 |
| commit | 927a76b4b1461ac549bc12f24c7bf73f610bd4e4 (patch) | |
| tree | f92d6c14e6d0ad1e17401a8dd1a822530d37eab2 /Test/vstte2012 | |
| parent | 23ad17c104cc8814c2b94a608386c0535f6d0f2f (diff) | |
Changed ranking function for Seq, so that it's compatible with data types.
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy index f51a36b2..7ce48fcc 100644 --- a/Test/vstte2012/RingBufferAuto.dfy +++ b/Test/vstte2012/RingBufferAuto.dfy @@ -55,6 +55,8 @@ 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];
|