[Why3-club] Variant on a recursive predicate in Why3 1.0.0

Kruer, Joseph C. jkruer at draper.com
Tue Jul 31 23:22:45 CEST 2018

I've written the following recursive predicate, below, and I'd like to prove that it terminates. I've added a suitable variant, but I am getting a vague syntax error for which I found no obvious remedy in the WIP documentation for 1.0.0 on the Why3's Gitlab. Any pointers in the right direction would be greatly appreciated.

predicate escapedUpto (d: array char) (u: int) =
                variant { u }
((u > 1 /\ d[u-1] = chr 22 \/ d[u-1] = chr 92 -> d[u-2] = chr 92) /\ (escapedUpto d (u-2)))
  (d[u-1] <> chr 22 /\ d[u-1] <> chr 92 /\ (escapedUpto d (u-1)))
  (u = 0)

- Jay

Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20180731/1856cfd4/attachment.html>

More information about the Why3-club mailing list