Hello Why3-ople,
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
end
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?
Thanks,
- Jay
________________________________
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.
________________________________
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
