search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

Refer to result of explicit operation in post condition #290

Closed ZoeA closed 9 years ago

ZoeA commented 9 years ago

I'd like to be able to add a post condition to an explicit operation that refers to the result returned by that operation. I believe there used to be a keyword for doing this (such as res) in overture, but this option doesn't seem to exist for CML? It would be nice to have this available in CML. Here is a simple example:

state
  counts : seq of nat := [0,0]

operations

  getCounts:nat==>nat
  getCounts(n) == (return counts(n))
  pre n in set inds counts
  post "result" = counts(n)
ZoeA commented 9 years ago

Richard suggested using "RESULT" (all caps) -- this was a variant I hadn't tried but it seems to work. I think that this can be closed now.

Thanks!