Commit 998ab112 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix broken specification of array.Array.defensive_set.

parent 201a01ad
...@@ -45,7 +45,7 @@ module Array ...@@ -45,7 +45,7 @@ module Array
let defensive_set (a: array 'a) (i: int) (v: 'a) let defensive_set (a: array 'a) (i: int) (v: 'a)
ensures { 0 <= i < length a /\ a = (old a)[i <- v] } ensures { 0 <= i < length a /\ a = (old a)[i <- v] }
raises { OutOfBounds -> i < 0 \/ i >= length a /\ a = old a } raises { OutOfBounds -> (i < 0 \/ i >= length a) /\ a = old a }
= if i < 0 || i >= length a then raise OutOfBounds; = if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v a[i] <- v
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment