--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [PROVENANCE INTERNET] Re: New Frama-C version: Fluorine



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>