Ex2.java

Ex3.java

BinarySearchSafety.java

BinarySearchSoundness.java

BinarySearchCompleteness.java

BinarySearchOverflow.java

BinarySearchOverflowFix.java

tri_safety.java

tri_injectivity.java

tri_sorted.java

Notez pour tri_sorted.java qu'il faut eventuellement augmenter le timeout pour qu'Alt-Ergo arrive a tout prouver. Notez aussi que l'invariant ligne 15, redondant avec celui ligne 16 (on pourrait donc l'enlever, mais en le laissant on aide Alt-Ergo).