, From Weakest Pre-Conditions to Victory Invariants We now state the main correctness result for our verification language, as a transfer property from language W G to games. Essentially, we claim that weakest pre-conditions for W G induce the existence of victory invariants

P. ,

P. G-=-{(x,-x)-?-p(g)-×-g-|-x-?-?,

Q. G-=-{(x,-x,-0,-y)-?-p(g)-×-g-×-{0}-×-g-|-y and ?. X}, We define the base specification context ? G associated to game G = (G, ?) as the single-element specification context mapping CONT

{. and Q. , We derive from Theorem 4 an immediate corollary, which concludes the existence of a victory invariant for a pair of sets definable in the meta-logic as long as we can

R. J. Wright and J. , ? {0}|? ? : {0} of W G , all formula pairs ? 0 , ? 1 well-typed in context ?, now : G, and all ?-assignations ?, if the contract satisfaction property C, Corollary 1. For all games G = (G, ?), all well-typed programs CONT : P(G), vol.27, pp.583-625, 1990.

R. Bornat, Proving pointer programs in Hoare logic, Mathematics of Program Construction, pp.102-126, 2000.

M. Clochard, Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels, 2018.

M. Clochard, A. Paskevich, and C. Marché, Deductive verification via ghost debugging, Research Report, vol.9219, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01907894

E. W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, vol.18, pp.453-457, 1975.
DOI : 10.1145/360933.360975

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, Formal Methods in System Design, vol.48, issue.3, pp.152-174, 2016.

R. Krebbers, R. Jung, A. Bizjak, J. H. Jourdan, D. Dreyer et al., The essence of higher-order concurrent separation logic, 26th European Symposium on Programming Languages and Systems, vol.10201, pp.696-723, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01633133

K. R. Leino, Dafny: An automatic program verifier for functional correctness, LPAR-16, vol.6355, pp.348-370, 2010.
DOI : 10.1007/978-3-642-17511-4_20

K. Mamouras, Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism, Logical Methods in Computer Science, vol.12, issue.3, 2016.

Z. Manna and J. Mccarthy, Properties of programs and partial function logic, Machine Intelligence, vol.5, 1970.

M. O. Myreen and M. J. Gordon, Tools and Algorithms for the Construction and Analysis of Systems, pp.568-582, 2007.

H. Schorr and W. M. Waite, An efficient machine-independent procedure for garbage collection in various list structures, Communications of the ACM, vol.10, pp.501-506, 1967.
DOI : 10.1145/363534.363554

H. Yang, Relational separation logic, Theoretical Computer Science, vol.375, issue.1, pp.308-334, 2007.
DOI : 10.1016/j.tcs.2006.12.036
URL : https://doi.org/10.1016/j.tcs.2006.12.036