--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on April 2013 ---
Sent from my Android No dia 19 de Abr de 2013 14:45, "Lo?c Correnson" <loic.correnson at cea.fr> escreveu: > Small detail about your Length axiomatic : > > axiomatic Length > { > logic integer Length{L}(char *s) reads *s; > > axiom string_length{L}: > \forall integer n, char *s ; Length_of_str_is(s, n) <==> Length(s) > == n ; > } > > This is over-specified. I choose only (==>) in my solution. > Actually, I'm afraid there is an inconsistency with (<==>). > Your axioms proves that for all pointer s, Length_of_str_is(s,Length(s)). > This means that all strings have a length. Which is false, indeed. > > L. > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/e932af48/attachment.html>