Missing modifies clause is not detected

[fpottier]

The following .ml file is accepted by Cameleer:

let write a =
  a.(0) <- 1
(*@ write a
    requires Array.length a > 0
    ensures a.(0) = 1 *)

I am surprised; I thought that in such a case, it is necessary to declare modifies a. Is this a bug, or is it the intended behavior?

[mariojppereira]

Good catch. In fact, I am currently not imposing modifies in OCaml implementations since Why3 automatically detects every writing effect. Hence, the OCaml to WhyML translation automatically introduces the appropriate modifies.

Would you be in favor of imposing modifies even for implementations? If so, your example would generate the following WhyML program:

  let write a
    writes { }
  = a[0] <- 1

which of course would be rejected by Why3 type-system.

[fpottier]

I would be in favor of enforcing the same discipline, regardless of whether the specification appears in an .ml or .mli file. Otherwise, this is confusing (and prevents copying/pasting).

[mariojppereira]

Okay, I will implement this.

[fpottier]

That said, we probably need to have a discussion about the meaning of (and the need for) modifies clauses in Gospel; this is related to the manner in which we wish to deal with aliasing and ownership in Gospel.