[Why3-club] Non-int equality

Guillaume Melquiond guillaume.melquiond at inria.fr
Thu Jul 19 08:11:59 CEST 2018


Le 18/07/2018 à 21:19, Kruer, Joseph C. a écrit :
> Hello Why3-ople,
> 
> I’m working on a verification task working with strings and therefore 
> find myself doing lots of individual character comparisons.

Just a disclaimer first. The char/string library has been designed seven 
years ago, and it has not evolved much since then. If it were to be 
designed from scratch today, it would certainly look a lot different. 
(And now that we are ready to have string literals in Why3, it will 
eventually get such a redesign.)

> My lingering questions at this point are essentially these:
> 
> 1.Does my solution of overloading (=) to operate on chars break 
> anything? Could I add it to the stdlib’s Char module?

This shows how little used this part of the standard library is. You are 
right; given the current definition of the char type, the module should 
have provided something like

val (=) (x y: char): bool ensures { result <-> x = y }

> 2.How does “logical equality” work? is it polymorphic?

Yes it is.

Program equality is also polymorphic from a typing point of view, but it 
is an error if, once an occurrence has been typed, it does not match 
exactly one program declaration.

> 3.How do the logical/non-logical “namespaces” of Why3 work?

Short version is: logical declarations ("function") are accessible when 
defining a logical function, program declarations ("let", "val") are 
accessible when defining a program function.

> 4.Could one add to Why3 a polymorphic equality operator for record types 
> that might be defined as, say, field-wise equality?

If you mean logical equality, then it already works that way.

For program equality, however, you have to define it explicitly on a 
per-type basis. In particular, as soon as your record has private or 
ghost features, field-wise equality is generally not the one you want.

Best regards,

Guillaume


More information about the Why3-club mailing list