Commit 91da3269 authored by MARCHE Claude's avatar MARCHE Claude

Fix incomplete specs of defensive set functions

parent 717baeab
......@@ -45,7 +45,7 @@ module Array
let defensive_set (a: array 'a) (i: int) (v: 'a)
ensures { 0 <= i < length a /\ a = (old a)[i <- v] }
raises { OutOfBounds -> i < 0 \/ i >= length a }
raises { OutOfBounds -> i < 0 \/ i >= length a /\ a = old a }
= if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
......
......@@ -45,7 +45,7 @@ module Matrix
let defensive_set (a: matrix 'a) (i: index) (v: 'a)
ensures { valid_index a i /\ a = set (old a) i v }
raises { OutOfBounds -> not (valid_index a i) }
raises { OutOfBounds -> not (valid_index a i) /\ a = old a }
= let r,c = i in
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set 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