The Merriam-Webster dictionnary defines an assumption as “a fact or statement (as a proposition, axiom, postulate, or notion) taken for granted”. This is indeed the role that assumptions play in formal verification of programs, as performed in Frama-C platform or GNATprove. Assumptions may either be related to the proof of a single function (like “this [...]
Want to get involved?
Contactinfo @ open-do.org