, Assign "over

, Assign "fact" (Const, vol.1

, Assign "i

, While (Not (Equal (Var "n") (Const 0))) ( Assign "a

, Assign "i" (Const, vol.1

, Var n))) ( Assign "fact" (Plus (Var "fact

, Assign "i" (Plus (Var "i") (Const 1)) )

, On commence par définir deux lemmes correspondant aux invariants des deux boucles et on montre le résultat suivant par récurrence (code), où rd fm state accèdeà une variable de l'état, et où fact calcule (mathématiquement) la factorielle. exists (x:flow_interp s_state)

M. Bodin, P. Gardner, T. Jensen, and A. Schmitt, Skeletal Semantics and their Interpretations, Proceedings of the ACM on Programming Languages, vol.44, pp.1-31, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01881863

A. Charguéraud, Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIG-PLAN international conference on Functional Programming, pp.418-430, 2011.

N. Courant, E. Crance, and A. Schmitt, Necro : Animating Skeletons, ML 2019, 2019.

R. Jung, R. Krebbers, and J. Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up : A modular foundation for higher-order concurrent separation logic, Journal of Functional Programming, vol.28, issue.20, 2018.

G. Kahn, Natural semantics, STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, vol.247, pp.22-39, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075953

L. Li and E. L. Gunter, Isak : A complete semantics of K, 2018.

, Grigore Ro?u. Matching logic. Logical Methods in Computer Science, vol.13, issue.4, pp.1-61, 2017.

G. Ro?u and . Traian-florin-?erb?nu??, An overview of the K semantic framework, Journal of Logic and Algebraic Programming, vol.79, issue.6, pp.397-434, 2010.

P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge et al., Ott : Effective tool support for the working semanticist, Journal of Functional Programming, vol.20, issue.1, pp.71-122, 2010.