## Inverting an Injection, in Why3

Inverting an injective array, in Why3

**Authors:** Jean-Christophe Filliâtre

**Topics:** Array Data Structure / Permutation

**Tools:** Why3

**References:** The 1st Verified Software Competition / The VerifyThis Benchmarks

see also the index (by topic, by tool, by reference, by year)

(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 2: inverting an injection Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) *) module InvertingAnInjection use int.Int use array.Array use map.MapInjection as M predicate injective (a: array int) (n: int) = M.injective a.elts n predicate surjective (a: array int) (n: int) = M.surjective a.elts n predicate range (a: array int) (n: int) = M.range a.elts n let inverting (a: array int) (b: array int) (n: int) : unit requires { n = length a = length b /\ injective a n /\ range a n } ensures { injective b n } = for i = 0 to n - 1 do invariant { forall j. 0 <= j < i -> b[a[j]] = j } b[a[i]] <- i done (* variant where array b is returned /\ with additional post *) let inverting2 (a: array int) (n: int) : array int requires { n = length a /\ injective a n /\ range a n } ensures { length result = n /\ injective result n /\ forall i. 0 <= i < n -> result[a[i]] = i } = let b = make n 0 in for i = 0 to n - 1 do invariant { forall j. 0 <= j < i -> b[a[j]] = j } b[a[i]] <- i done; b end module Test use array.Array use InvertingAnInjection 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 } end

download ZIP archive

# Why3 Proof Results for Project "vstte10_inverting"

## Theory "vstte10_inverting.InvertingAnInjection": fully verified

Obligations | Alt-Ergo 2.0.0 | CVC3 2.4.1 | CVC4 1.5 | Coq 8.11.2 | Z3 4.6.0 | ||

VC for inverting | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||

loop invariant init | 0.01 | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | ||

loop invariant preservation | --- | 0.00 | --- | --- | --- | ||

postcondition | --- | --- | --- | 0.31 | --- | ||

postcondition | 0.00 | --- | --- | --- | --- | ||

VC for inverting2 | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||

array creation size | 0.01 | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | ||

index in array bounds | 0.00 | --- | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | ||

postcondition | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||

VC for inverting2 | 0.00 | --- | --- | --- | --- | ||

VC for inverting2 | --- | --- | --- | 0.34 | --- | ||

VC for inverting2 | 0.01 | 0.01 | 0.01 | --- | 0.00 | ||

out of loop bounds | 0.00 | --- | --- | --- | --- |

## Theory "vstte10_inverting.Test": fully verified

Obligations | Alt-Ergo 2.0.0 | |

VC for test | --- | |

split_goal_right | ||

array creation size | 0.01 | |

index in array bounds | 0.01 | |

index in array bounds | 0.01 | |

index in array bounds | 0.00 | |

index in array bounds | 0.01 | |

index in array bounds | 0.01 | |

index in array bounds | 0.02 | |

index in array bounds | 0.01 | |

index in array bounds | 0.01 | |

index in array bounds | 0.01 | |

index in array bounds | 0.01 | |

assertion | 0.04 | |

precondition | 0.13 | |

assertion | 0.39 |