search

ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
37 stars 10 forks source link

Adapt warning message for ensures not found #152

Closed n-osborne closed 11 months ago

n-osborne commented 11 months ago

This PR proposes a new warning message when the next_state case cannot be computed with the ensures clauses present in the specifications.

This is an attempt to answer point 4 in #150

shym commented 11 months ago

I (force-)pushed a proposed reformulation.

n-osborne commented 11 months ago

Thanks. I like the error message better now.