--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on September 2013 ---
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