Longest Common Prefix (Quantified Permissions)

/* First task of the longest common prefix problem from * VerifyThis@FM2012: http://fm2012.verifythis.org/challenges */ define access(a) forall k: Int :: 0 <= k && k < len(a) ==> acc(loc(a, k).val) define untouched(a) forall k: Int :: 0 <= k && k < len(a) ==> loc(a, k).val == old(loc(a, k).val) /* Task A */ // used to write matching trigger terms below function offset(k:Int, x:Int, y:Int) : Int { y + k - x } method lcp(a: IArray, x: Int, y: Int) returns (n: Int) requires access(a) requires 0 <= x && 0 <= y && x < len(a) && y < len(a) ensures access(a) ensures 0 <= n && x + n <= len(a) && y + n <= len(a) ensures forall k: Int :: {loc(a, offset(k,x,y))} // instantiation trigger term x <= k && k < x + n ==> loc(a, k).val == loc(a, offset(k,x,y)).val /* The following postcondition is logically equivalent to the previous one, and a bit * easier to understand. However, it can currently not be used because it contains * no possible triggers (due to the arithmetic operations inside the loc-expressions). */ // ensures forall k: Int :: 0 <= k && k < n ==> loc(a, x + k).val == loc(a, y + k).val ensures x + n < len(a) && y + n < len(a) ==> loc(a, x + n).val != loc(a, y + n).val { n := 0 while (x + n < len(a) && y + n < len(a) && loc(a, x + n).val == loc(a, y + n).val) invariant n >= 0 invariant access(a) invariant x + n <= len(a) && y + n <= len(a) invariant forall k: Int :: {loc(a, offset(k,x,y))} // instantiation trigger term x <= k && k < x + n ==> loc(a, k).val == loc(a, offset(k,x,y)).val { n := n + 1 } } /* Encoding of arrays */ field val: Int domain IArray { function loc(a: IArray, i: Int): Ref function len(a: IArray): Int function first(r: Ref): IArray function second(r: Ref): Int axiom all_diff { forall a: IArray, i: Int :: {loc(a, i)} first(loc(a, i)) == a && second(loc(a, i)) == i } axiom length_nonneg { forall a: IArray :: len(a) >= 0 } }