--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on November 2011 ---
Hello, in a recent case study, I argue that using the strongest postcondition calculus to automatically infer postconditions may significantly reduce annotation effort (I discussed this some time ago at Fraunhofer FIRST). For example, consider this code, where the postcondition can be derived from the code. /*@ requires \valid(this); @ ensures this->active && this->target_speed == speed; */ void set(device_t *this, int speed) { this->active = true; this->target_speed = speed; } To support this hypothesis, it would be useful to add strongest postconditions to Frama-C/Jessie. If the goal is to have a proof-of-concept demonstrator for my toy code (which is loop-free), what effort would be required to do so (in terms of time, people and skill)? Should this be implemented as a Frama-C plug in? -- Best regards, Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111114/0ad448bd/attachment.htm>