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)
Thanks,
- 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.
________________________________
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
