Progress at last
This afternoon, I finally managed to get InforML to acceptably process one of my key examples. You start by defining some abstract data type
module rational : sig
label Rat
type rat : (Lab -> * @ Rat) @ ⊥
fun fromInt : 〈l:Lab〉 ((Int @ l) -(l)-> (rat @ l)) @ ⊥
# Approximates to the nearest integer
fun toInt : ((rat @ ⊥) -(⊤)-> (Int @ ⊥)) @ ⊥
end = mod
newlabel Rat
type rat : (Lab -> * @ Rat) @ ⊥ = (fn l:Lab => (Int @ l, Int @ l) end)
fun fromInt : 〈l:Lab〉 ((Int @ l) -(l)-> (rat @ l)) @ ⊥
fun fromInt 〈l:Lab〉 (i : Int @ l) : rat @ l = (i, 1)
# Notice this is a more general type than the one
# exposed by the signature
fun toInt : 〈l:Lab〉 ((rat @ l) -(l)-> (Int @ l)) @ ⊥
fun toInt 〈l:Lab〉 ((i1, i2) : rat @ l) : Int @ l = i1 div i2
end
The important thing to note here is that the abstraction assumes the invariant that the second integer in the pair will never become zero. Next you define a malicious function using type analysis
fun badtcase 〈p:Lab (b:* @ p)〉 (x:b) : b =
typecase b
of (Int @ p, Int @ p) => (1,0)
| _ => (x : b)
end
Now you use your malicious function to create an invalid instance of the abstract data type
val x : (rational.rat @ rational.Rat)
And finally notice that this new corrupted value of the abstract data type cannot be used to cause a divide by zero, as
has an information content of rational.Rat which is greater than ⊥ as specified by the signature.
Yes, I know that WordPress obliterated my whitespace, but I don't really feel like trying to fix it by hand at the moment. It also seems to enjoy converting all my <div> tags into <p> tags.