Commit 340ffc11 authored by Andrei Paskevich's avatar Andrei Paskevich

examples/vstte10_queens: strong updates

1. Strong region updates can only work with direct assignments, e.g.
     r.contents <- something_completely_different
   but not with functions such as (:=) : ref 'a -> 'a -> unit
   Why3 requires 'a to be instantiated with one concrete type,
   not with a bunch of types that differ in their regions.

2. Strong region updates will restrict the updated regions to their
   covers. However, in the current implementation, Why3 does not know
   if the region corresponding to the field "contents" is the only
   cover for 'a in the type [ref 'a] or if there is a way to retrieve
   'a from [ref 'a] without going through "contents". Therefore, to
   ensure soundness, a strong update of r.contents will forbid to
   use r itself. A solution consists in writing an adhoc "reference"
   type, where the mutable contents (O.t in this case) is explicitly
   given in the type definition. Then the strong update of the field
   containing O.t will preserve the covering "reference".

   This problem is fixed in the "new system", where mutable types
   carry information about the access paths of the type variables.
   There, "r.contents <- something_different" preserves r.
parent 312f137e
......@@ -185,7 +185,7 @@ module MachineArithmetic
use mach.onetime.OneTime as O
type oref = { mutable ot : O.t }
let rec mcount_bt_queens (board: array int63) (n: int63) (pos: int63) : O.t
requires { to_int (length board) = to_int n }
......@@ -197,7 +197,7 @@ module MachineArithmetic
if eq pos n then
O.succ ( ())
else begin
let s = ref ( ()) in
let s = { ot = () } in
let rec forloop (i: int63) = (* for i = 0 to n-1 do *)
requires { 0 <= to_int i <= to_int n }
requires { is_board board (to_int pos) }
......@@ -206,13 +206,13 @@ module MachineArithmetic
if i < n then begin
board[pos] <- i;
if mcheck_is_consistent board pos then
s := O.add !s (mcount_bt_queens board n (pos + of_int 1));
s.ot <- O.add s.ot (mcount_bt_queens board n (pos + of_int 1));
(* let _ = O.add !s (mcount_bt_queens board n (pos + of_int 1))
in (); *)
forloop (i + of_int 1)
end in
forloop (of_int 0);
let mcount_queens (board: array int63) (n: int63) : O.t
......@@ -225,7 +225,5 @@ module MachineArithmetic
let a = Array63.make n (of_int 0) in
mcount_queens a n
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment