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

[Frama-c-discuss] Introductory slides on Frama-C



Great !
	L.

Le 3 sept. 2013 ? 23:45, Yannick Moy <moy at adacore.com> a ?crit :

> -- David MENTRE (2013-09-03)
>> 
>> I tried to present an up-to-date view of Frama-C and its ecosystem.
>> 
>> I would be glad to get any feedback about them: error, things to improve, etc.
> 
> Nice tour!
> 
>> In slide 47, behaviours found and not_found have opposite logical condition for assumes clauses. However I find difficult to explain it without going back to first order logic (!(a ==> b) eq. !(!a || b) eq. ...) which I would like to avoid. Any idea on a way to explain that simply?
> 
> I would explain it starting with the simpler assumes:
> 
>  \exists index i; a[i] == v
>  \forall index i; a[i] != v
> 
> which clearly are complementary propositions. Then you can explain that they are equivalent to the propositions you wrote on your slide.
> --
> Yannick Moy, Senior Software Engineer, AdaCore
> 
> 
> 
> 
> 
> _______________________________________________
> 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