search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Inconsistent use of arrow types #47

Open robin-aws opened 2 years ago

robin-aws commented 2 years ago

There is a decent mix of ->, -->, and ~> arrow types in this repo, owing mostly to personal taste and/or willingness to spend the time generalizing. Ideally all code would be maximally general and use ~>, but that does lead to more complicated specifications and verification so it is not free.

Should we add this to the style guide? Or even a CI mechanism to insist on ~>?

MikaelMayer commented 2 years ago

Good questions. I think we can always promote -> to --> and then to~>` for arguments when it will be necessary, correct?

cpitclaudel commented 2 years ago

Correct @MikaelMayer, but that entails additional proof obligations (the preconditions of the more general function that you're calling).

MikaelMayer commented 2 years ago

That's part of the upgrade, but for a user of the library, that wouldn't be a breaking change, would it?

cpitclaudel commented 2 years ago

that wouldn't be a breaking change, would it?

It could be, since the new proofs are harder. It may be that Dafny managed to call the previous function with the simpler spec and not the one with the more general spec.

For example Map(f: A -> B, xs: seq<A>) has no preconditions. But Map(f: A --> B, xs: seq<A>) has requires forall a | a in xs :: f.requires(a). It should be easy to satisfy this new precondition, but it's still extra work.

Sometimes it's worse, and the most general version of the function has complex preconditions that can be satisfied in various ways that are not immediately obvious (for example, Fold)