[Why3-club] strange loops in the sequence library

Sandrine Blazy Sandrine.Blazy at irisa.fr
Tue Feb 26 09:40:47 CET 2019


in the library of sequences, several definitions use a while loop that is never executed.
For instance, the function set <> (s:seq <http://why3.lri.fr/stdlib/seq.html#seq_14> 'a) (i:int) (v:'a) : seq <http://why3.lri.fr/stdlib/seq.html#seq_14> 'a starts with
while false do variant { 0 } () done;
Are these loops mandatory ?

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190226/34661e6f/attachment.html>

More information about the Why3-club mailing list