Implementation guidance for the adoption of SPARK, 2018. ,
Deductive Software Verification -The KeY Book -From Theory to Practice, and Mattias Ulbrich, vol.10001, 2016. ,
Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification, 2019. ,
Leveraging rust types for modular specification and verification, Proc. ACM Program. Lang, vol.3, 2019. ,
Let's verify this with Why3, International Journal on Software Tools for Technology Transfer (STTT), vol.17, issue.6, pp.709-727, 2015. ,
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
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 installation instructions
, OpenJML pull request 691
, Eclipse installation packages
Code source en Java de ParcourSup ,
Document de présentation des algorithmes de ParcourSup ,
Site principal de ParcourSup ,
VeriFast: A powerful, sound, predictable, fast verifier for C and Java, NASA Formal Methods, vol.6617, pp.41-55, 2011. ,
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
The Dafny integrated development environment, Proceedings 1st Workshop on Formal Integrated Development Environment, vol.149, pp.3-15, 2014. ,
The Krakatoa tool for deductive verification of Java programs, Winter School on Object-Oriented Verification, 2009. ,
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. ,
Étude formelle de l'implémentation du code des impôts, Trente-et-unièmes Journées Francophones des Langages Applicatifs, 2020. ,
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
,
, 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
forall i: usize :: (0 ? i && i < result.len()) ==> result[i].rang == (i+1) as i32 ,
, before _ expiry(result)[i] == voeux _ classes
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