Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] SP calculus

  • Subject: [Frama-c-discuss] SP calculus
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Mon, 14 Nov 2011 12:59:48 +0100
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>