--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on November 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] SP calculus



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>