[Why3-club] Non-int equality
Kruer, Joseph C.
jkruer at draper.com
Wed Jul 18 21:19:47 CEST 2018
I'm working on a verification task working with strings and therefore find myself doing lots of individual character comparisons. I ran into an error that left me scratching my head for a bit in something like the following code:
let headIsA (s: list char) : bool =
match HdTl.hd s with
| Some(c) -> c = Char.chr 41
| None -> False
This causes Why3 to raise the following error: "This expression has type char, but is expected to have type int". I'm fairly certain now that this is because (=) is defined in the Int module as a binary operation on ints. My initial solution to this was to explicitly use c.code (which is a private field of the record type char) and compare against the integer value of the character in question. Another idea I had that felt a bit nicer was to define a pure function (=) taking a pairs of ints to bools, but this raised another error: "Logical equality cannot be redefined." Finally I defined it as a method with an ensures clause like Int's (=) which did the trick.
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?
2. How does "logical equality" work? is it polymorphic?
3. How do the logical/non-logical "namespaces" of Why3 work?
4. Could one add to Why3 a polymorphic equality operator for record types that might be defined as, say, field-wise equality?
Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club