From 7e909f86c777b12ad55c3efd2b68b1d3c8adfda4 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Date: Wed, 18 Jul 2012 18:12:33 +0200 Subject: [PATCH] new example: distance (in progress) --- examples/programs/distance.mlw | 76 ++++ examples/programs/distance/why3session.xml | 493 +++++++++++++++++++++ 2 files changed, 569 insertions(+) create mode 100644 examples/programs/distance.mlw create mode 100644 examples/programs/distance/why3session.xml diff --git a/examples/programs/distance.mlw b/examples/programs/distance.mlw new file mode 100644 index 000000000..64f9f8ea2 --- /dev/null +++ b/examples/programs/distance.mlw @@ -0,0 +1,76 @@ + +(* + Author: Jean-Christophe Filliatre (CNRS) + Tool: Why3 (see http://why3.lri.fr/) + + The following problem was suggested to me by Ernie Cohen (Microsoft Research) + + We are given an integer N>0 and a function f such that 0 <= f(i) < i + for all i in 0..N-1. We define a reachability as follows: + each integer i in 0..N-1 can be reached from any integer in f(i)..i-1 + in one step. + + The problem is then to compute the distance from 0 to N-1 in O(N). + Even better, we want to compute this distance, say d, for all i + in 0..N-1 and to build a predecessor function g such that + + i <-- g(i) <-- g(g(i)) <-- ... <-- 0 + + is the path of length d[i] from 0 to i. +*) + +module Distance + + use import int.Int + use import module ref.Refint + use import module array.Array + + (* parameters [N] and [f] are introduced as logic symbols *) + constant n: int + axiom n_nonneg: 0 < n + + function f int: int + axiom f_prop: forall k: int. 0 <= k < n -> 0 <= f k < k + + (* path from 0 to i of distance d *) + inductive path int int = + | path0: path 0 0 + | paths: forall i: int. 0 <= i < n -> + forall d j: int. path d j -> f i <= j < i -> path (d+1) i + + predicate distance (d i: int) = + path d i /\ forall d': int. path d' i -> d <= d' + + (* function [g] is built in an array and then returned *) + let distance () = + { } + let g = make n 0 in + g[0] <- -1; (* sentinel *) + let d = make n 0 in + d[0] <- 0; (* redundant *) + let count = ref 0 in (* ghost *) + for i = 1 to n-1 do + invariant { g[0] = -1 /\ + (forall k: int. 0 < k < i -> f k <= g[k] < k) /\ + (forall k: int. 0 < k < i -> d[k] = d[g[k]] + 1) (* /\ + (forall k: int. 0 <= k < i -> path d[k] k) *) } + let j = ref (i-1) in + while g[!j] >= f i do + invariant { f i <= !j < i } + variant { !j } + j := g[!j]; + incr count + done; + d[i] <- 1 + d[!j]; + g[i] <- !j + done; + g + { forall k: int. 0 < k < n -> f k <= result[k] < k } + +end + +(* +Local Variables: +compile-command: "why3ide distance.mlw" +End: +*) diff --git a/examples/programs/distance/why3session.xml b/examples/programs/distance/why3session.xml new file mode 100644 index 000000000..7fd363ef8 --- /dev/null +++ b/examples/programs/distance/why3session.xml @@ -0,0 +1,493 @@ + + + + + + + + + + + + -- 2.26.2