In precept, we defined a relation between
two implementations of a range (ListRange
and LoHiPairRange):
let abs (lr:ListRange) (pr:LoHiPairRange) =
(hd lr , hd (rev lr)) = pr
We also laid out the proof obligation for
showing that the relationship between the
module persists through their APIs:
Forall k:int:
abs (L.singleton k) (P.singleton k) = true
Forall i,j:int:
abs (L.range i j) (P.range i j) = true
Forall l:(int list), p:(int*int), k:int:
if (L.inv l) and (P.inv p) and (abs l p) then
abs (L.(+) l k) (P.(+) p k) = true
Forall l:(int list), p:(int*int), k:int:
if (L.inv l) and (P.inv p) and (abs l p) then
abs (L.(*) l k) (P.(*) p k) = true
Forall l1,l2:(int list), p1,p2:(int*int):
if (L.inv l1) and (L.inv l2) and (P.inv p1) and (P.inv p2)
and (abs l1 p1) and (abs l2 p2) then
(abs (L.bridge l1 l2) (P.bridge p1 p2)) = true
Forall l:(int list), p:(int*int):
if (L.inv l) and (P.inv p) and (abs l p) then
L.size l = P.size p
Forall l:(int list), p:(int*int), k:int:
if (L.inv l) and (P.inv p) and (abs l p) then
L.contains l k = P.contains p k
Forall l1,l2:(int list), p1,p2:(int*int):
if (L.inv l1) and (L.inv l2) and (P.inv p1) and (P.inv p2)
and (abs l1 p1) and (abs l2 p2) then
L.(<) l1 l2 = None and P.(<) p1 p2 = None
OR
L.(<) l1 l2 = Some b and P.(<) p1 p2 = Some b' and b=b'.
This week's exercise is to work through these proofs, but because of
the complicated implementation of ListRange, it may be more beneficial
to complete the proofs for a different implementation, such as
LoLenPairRange.
recall: let LHPR.inv = (lo <= hi)
and consider: let LLPR.inv = (len > 0)
let abs (llpr:LoLenPairRange) (lhpr:LoHiPairRange) =
let (lo, len) = llpr in
(lo, lo+len-1) = lhpr