search

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
124 stars 16 forks source link

Limit `modifies` terms #2

Open pascutto opened 3 years ago

pascutto commented 3 years ago

consumes and modifies declarations currently accept any terms. These should be restricted to qualified identifiers only e.g. x.y.z.

backtracking commented 3 years ago

Do we want to allow x.(old y).z?

mariojppereira commented 3 years ago

Do we want to allow x.(old y).z?

That is very interesting, indeed :) I believe this would make sense only for consumes, right? A modifies clause containing an old seems odd to me.

backtracking commented 3 years ago

Here is an example where modifies x.(old y).z would make sense:

type t = { mutable y: int ref }
let f (x: t) = x.y := 0; x.y <- ref 0