From c7df83f7abe88c8cc8fc2c8520721e1bc9b634f7 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Fri, 1 Jun 2018 09:16:59 +0200 Subject: [PATCH] new example: minimum excludant --- examples/mex.mlw | 49 +++++++++++++++++ examples/mex/why3session.xml | 99 +++++++++++++++++++++++++++++++++++ examples/mex/why3shapes.gz | Bin 0 -> 1223 bytes 3 files changed, 148 insertions(+) create mode 100644 examples/mex.mlw create mode 100644 examples/mex/why3session.xml create mode 100644 examples/mex/why3shapes.gz diff --git a/examples/mex.mlw b/examples/mex.mlw new file mode 100644 index 000000000..52d57af34 --- /dev/null +++ b/examples/mex.mlw @@ -0,0 +1,49 @@ + +(* {1 Minimum excludant, aka mex} + + Given a finite set of integers, find the smallest nonnegative integer + that does not belong to this set. +*) + +module MexArray + + use import int.Int + use import map.Map + use import array.Array + use import ref.Refint + use import pigeon.Pigeonhole + + predicate mem (x: int) (a: array int) = + exists i. 0 <= i < length a && a[i] = x + + let mex (a: array int) : int + ensures { 0 <= result <= length a } + ensures { not (mem result a) } + ensures { forall x. 0 <= x < result -> mem x a } + = let n = length a in + let used = make n false in + let ghost idx = ref (fun i -> i) in + for i = 0 to n - 1 do + invariant { forall x. 0 <= x < n -> used[x] -> + mem x a && 0 <= !idx x < n && a[!idx x] = x } + invariant { forall j. 0 <= j < i -> 0 <= a[j] < n -> + used[a[j]] && 0 <= !idx a[j] < n && a[!idx a[j]] = a[j] } + let x = a[i] in + if 0 <= x && x < n then begin used[x] <- true; idx := set !idx x i end + done; + let r = ref 0 in + let ghost posn = ref (-1) in + while !r < n && used[!r] do + invariant { 0 <= !r <= n } + invariant { forall j. 0 <= j < !r -> used[j] && 0 <= !idx j < n } + invariant { if !posn >= 0 then 0 <= !posn < n && a[!posn] = n + else forall j. 0 <= j < !r -> a[j] <> n } + variant { n - !r } + if a[!r] = n then posn := !r; + incr r + done; + if !r = n && !posn >= 0 then pigeonhole (n+1) n (set !idx n !posn); + !r + +end + diff --git a/examples/mex/why3session.xml b/examples/mex/why3session.xml new file mode 100644 index 000000000..e02a704f7 --- /dev/null +++ b/examples/mex/why3session.xml @@ -0,0 +1,99 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/mex/why3shapes.gz b/examples/mex/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..0892068f6cadfae7aeaae448e9e3724ad0599de6 GIT binary patch literal 1223 zcmV;&1UUO2iwFP!00000|J_&LZyPrZe)nJD_o4vxgAxfe!-`=61`OTHa4*9iD2duU zH0Q!e3U7b?c!?dKV<%0wVjGqQsif2K_>rGJksezsiU}NZQ)mf2M4vEb\$X!I2!#B&m z-YlHY7Kv zkOZmblw9EEvjmQD`F_3ruw0EFWwVm;#zw1~2LxBE?KJr5XOX>2r|`gFxl7r~_Qe0w z&3*_&m^P2|*gd^J4mjZDWZJT8ugQX>sJ9z)zl26LjCxTGW_mYG3L`*\$_#iZ%h{_f~g*0*E3K499N z8j)jn7XY;d0-p&gbY;Poy_1*{g%UD-!tQo&ck=tl^mb9J_RQGDIUmVE;}8R5ZKO?I z%8#@9VWZc&`FO|r=dvrSwmnPD-Gj3kxqo(`91E31w-TJ|l>\$3)AsbgZXs;0+`iTFx zTrgB`3RhJNQO?|b6O0{*3JKI_)b7rSBbV\$taNgcSXqusvUZIg->8@KGS;Uv;>>VL` z4(-zjcc`LdW}P&=HH}!Q2`gc%0@\$-ZIqj1dt9R\$pHyFf2SpfC;N`}jG@6^|B=KS\$& zijpntuTUFX(5mO@4)!sZB+TMN>MmN5B4Cmz\$ z`l3c-W3E0*XwgeGRCW4?n\$T_`dcmoDb79{aAH!&37g#lpXrvNKY7W)d%DpA%q%X1i zjLZORQ~*j`nyaO-Lh)ai6Wv*TZ-*pe(tuG?v~om|A_r&3|3qqD%88O9P4b^q zJ4NkIipgX1-IJCo{-5PUl4P{#&DRdeqG(ZVIT%itjGvMJt7UV`n3sm-=EV5L)8dGbqIH~!yX4-Hu>fbQ?\$Eo4p843| zU1Mp+#6U78GJIsWrDjuqMk8}H28zp_9yzivSxN~tDw>)XBR>{rmAKj^jwb\$O<<)Y1 zd\$U~kd#2nA{C&&oMGi#pv;J@*g5S5iZjR4p=RgncwB-#\$oQ?6&+2U^W\${NU7!y9LN lCX?~0em7Zro-bt_VBYM)yxE;!x%>APe*zIb8Uzy%001Q@awz}+ literal 0 HcmV?d00001 -- GitLab