vstte10_inverting.mlw 1.85 KB
 Jean-Christophe Filliatre committed Jun 22, 2011 1 2 3 4 ``````(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 2: inverting an injection `````` Jean-Christophe Filliatre committed Jul 05, 2011 5 6 `````` Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) `````` Jean-Christophe Filliatre committed Jun 22, 2011 7 ``````*) `````` 8 `````` `````` Jean-Christophe Filliatre committed Jun 21, 2011 9 ``````module InvertingAnInjection `````` 10 `````` `````` Andrei Paskevich committed Jun 15, 2018 11 12 `````` use int.Int use array.Array `````` MARCHE Claude committed Jul 13, 2011 13 `````` use map.MapInjection as M `````` 14 `````` `````` MARCHE Claude committed Jul 13, 2011 15 `````` predicate injective (a: array int) (n: int) = M.injective a.elts n `````` 16 `````` `````` MARCHE Claude committed Jul 13, 2011 17 `````` predicate surjective (a: array int) (n: int) = M.surjective a.elts n `````` 18 `````` `````` MARCHE Claude committed Jul 13, 2011 19 `````` predicate range (a: array int) (n: int) = M.range a.elts n `````` 20 `````` `````` Jean-Christophe Filliatre committed Mar 22, 2018 21 `````` let inverting (a: array int) (b: array int) (n: int) : unit `````` Andrei Paskevich committed Jan 30, 2013 22 `````` requires { n = length a = length b /\ injective a n /\ range a n } `````` Jean-Christophe Filliatre committed Mar 22, 2018 23 `````` ensures { injective b n } `````` Andrei Paskevich committed Oct 13, 2012 24 `````` = for i = 0 to n - 1 do `````` Jean-Christophe Filliatre committed Mar 22, 2018 25 `````` invariant { forall j. 0 <= j < i -> b[a[j]] = j } `````` Jean-Christophe Filliatre committed Jun 21, 2011 26 `````` b[a[i]] <- i `````` Jean-Christophe Filliatre committed Jan 24, 2011 27 `````` done `````` 28 `````` `````` Andrei Paskevich committed Jun 29, 2011 29 `````` (* variant where array b is returned /\ with additional post *) `````` Jean-Christophe Filliatre committed Jun 21, 2011 30 `````` `````` Jean-Christophe Filliatre committed Mar 22, 2018 31 `````` let inverting2 (a: array int) (n: int) : array int `````` Andrei Paskevich committed Jan 30, 2013 32 `````` requires { n = length a /\ injective a n /\ range a n } `````` Jean-Christophe Filliatre committed Mar 22, 2018 33 34 `````` ensures { length result = n /\ injective result n /\ forall i. 0 <= i < n -> result[a[i]] = i } `````` Andrei Paskevich committed Oct 13, 2012 35 `````` = let b = make n 0 in `````` Jean-Christophe Filliatre committed Jun 21, 2011 36 `````` for i = 0 to n - 1 do `````` Jean-Christophe Filliatre committed Mar 22, 2018 37 `````` invariant { forall j. 0 <= j < i -> b[a[j]] = j } `````` Jean-Christophe Filliatre committed Jun 21, 2011 38 39 40 41 42 43 44 45 `````` b[a[i]] <- i done; b end module Test `````` Andrei Paskevich committed Jun 15, 2018 46 47 `````` use array.Array use InvertingAnInjection `````` Jean-Christophe Filliatre committed Jun 21, 2011 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 `````` let test () = let a = make 10 0 in a[0] <- 9; a[1] <- 3; a[2] <- 8; a[3] <- 2; a[4] <- 7; a[5] <- 4; a[6] <- 0; a[7] <- 1; a[8] <- 5; a[9] <- 6; assert { a[0] = 9 && a[1] = 3 && a[2] = 8 && a[3] = 2 && a[4] = 7 && a[5] = 4 && a[6] = 0 && a[7] = 1 && a[8] = 5 && a[9] = 6 }; let b = inverting2 a 10 in assert { b[0] = 6 && b[1] = 7 && b[2] = 3 && b[3] = 1 && b[4] = 5 && b[5] = 8 && b[6] = 9 && b[7] = 4 && b[8] = 2 && b[9] = 0 } `````` Jean-Christophe Filliatre committed Dec 29, 2010 87 ``end``