T. Adacore, Implementation guidance for the adoption of SPARK, 2018.

W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, and P. H. Schmitt, Deductive Software Verification -The KeY Book -From Theory to Practice, and Mattias Ulbrich, vol.10001, 2016.

L. Andrès, Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification, 2019.

V. Astrauskas, P. Müller, F. Poli, and A. J. Summers, Leveraging rust types for modular specification and verification, Proc. ACM Program. Lang, vol.3, 2019.

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Let's verify this with Why3, International Journal on Software Tools for Technology Transfer (STTT), vol.17, issue.6, pp.709-727, 2015.

S. Boldo, J. Jourdan, X. Leroy, and G. Melquiond, Verified Compilation of Floating-Point Computations, Journal of Automated Reasoning, vol.54, issue.2, pp.135-163, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00862689

R. David, . Cok, and . Openjml, Software verification for Java 7 using JML, OpenJDK, and Eclipse, Proceedings 1st Workshop on Formal Integrated Development Environment, vol.149, pp.79-92, 2014.

. Openjml-contributors and . Openjml,

, OpenJML installation instructions

, OpenJML pull request 691

, Eclipse installation packages

H. Gimbert, Code source en Java de ParcourSup

H. Gimbert, Document de présentation des algorithmes de ParcourSup

H. Gimbert, Site principal de ParcourSup

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A powerful, sound, predictable, fast verifier for C and Java, NASA Formal Methods, vol.6617, pp.41-55, 2011.

N. Kosmatov, C. Marché, Y. Moy, and J. Signoles, Static versus dynamic verification in Why3, Frama-C and SPARK, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), vol.9952, pp.461-478, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01344110

K. Rustan, M. Leino, and V. Wüstholz, The Dafny integrated development environment, Proceedings 1st Workshop on Formal Integrated Development Environment, vol.149, pp.3-15, 2014.

C. Marché, The Krakatoa tool for deductive verification of Java programs, Winter School on Object-Oriented Verification, 2009.

C. Marché, C. Paulin-mohring, and X. Urbain, The Krakatoa tool for certification of Java/JavaCard programs annotated in JML, Journal of Logic and Algebraic Programming, vol.58, issue.1-2, pp.89-106, 2004.

D. Merigoux, R. Monat, and C. Gaie, Étude formelle de l'implémentation du code des impôts, Trente-et-unièmes Journées Francophones des Langages Applicatifs, 2020.

R. Rieu-helft, C. Marché, and G. Melquiond, How to get an efficient yet verified arbitrary-precision integer library, 9th Working Conference on Verified Software: Theories, Tools, and Experiments, vol.10712, pp.84-101, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519732

, collections::VecDeque

, est _ boursier: bool, 8 est _ resident: bool, 9 rang _ appel, p.32

, fn new(rang: i32, est _ boursier: bool, est _ resident: bool) ? VoeuClasse { 14

. Voeuclasse-{-rang and . Boursier,

, fn compare(voeux _ classes: Vec<VoeuClasse>, v: VoeuClasse) ? bool { 20 v == voeux _ classes

#. , ? i && i < voeux _ classes.len()) ==> voeux _ classes

, 0 ? taux _ min _ boursiers _ pourcents && taux _ min _ boursiers _ pourcents ? 100

, 0 ? taux _ min _ residents _ pourcents && taux _ min _ residents _ pourcents ? 100

. #[ensures=, forall i: usize :: (0 ? i && i < result.len()) ==> result[i].rang == (i+1) as i32

, before _ expiry(result)[i] == voeux _ classes

/. ^^todo, How to test for physical equality? 33 fn groupe _ classement( 34 voeux _ classes: Vec<VoeuClasse>, 35 taux _ min _ boursiers _ pourcents: i32, 36 taux _ min _ residents _ pourcents, p.32

, = voeux _ classes.len(

, 39 let mut br: VecDeque<VoeuClasse> = VecDeque::new(

, 40 let mut bnr: VecDeque<VoeuClasse> = VecDeque::new(

, 41 let mut nbr: VecDeque<VoeuClasse> = VecDeque::new(

, 42 let mut nbnr: VecDeque<VoeuClasse> = VecDeque::new(); _ boursiers _ total = br.len() as i32 + bnr.len(, vol.as, p.32

, 60 let nb _ residents _ total = br.len() as i32 + nbr.len(, vol.32

, let mut ordre _ appel : Vec<VoeuClasse> = Vec::new(); _ boursiers _ restants = br.len() as i32 + bnr.len(, vol.as, p.32

, 68 let nb _ residents _ restants = br.len() as i32 + nbr.len(, vol.32

, 69 let nb _ boursiers _ appeles = nb _ boursiers _ total -nb _ boursiers _ restants

, 70 let nb _ residents _ appeles = nb _ residents _ total -nb _ residents _ restants; _ taux _ boursiers = 0 < nb _ boursiers _ restants && (nb _ boursiers _ appeles * 100 < taux _ min _ boursiers _ pourcents * (1 + nb _ appeles

, 74 let contrainte _ taux _ residents = 0 < nb _ residents _ restants