Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Detecting undefined


view this post on Zulip Email Gateway (Jan 09 2021 at 19:32):

From: David Kretzmer <david.k@posteo.de>
Hello,

I am developing an executable operational semantics for a programming
language in Isabelle/HOL. One area that makes me a bit uneasy is the
existence of undefined. Since the occurrence of undefined may
indicate a bug in the semantics (e.g., an off-by-one error when indexing
into a list) and also raises an exception during execution, I would like
to prove that any final execution state obtained by the transition
relation is independent of undefined.

However, as undefined is a undetermined yet legal value there does not
seem a way to express this property. The only alternative I see is to
prove the much stronger property that any final execution state is part
of a set of known, valid states. However, I would like to start with the
simpler property (i.e., no undefined). Is this possible?

Best regards,
David

view this post on Zulip Email Gateway (Jan 11 2021 at 11:35):

From: Tobias Nipkow <nipkow@in.tum.de>
Undefined means "underdefined" - it is some value, but we don't know which one.
Proving that something is different from undefined is not very meaningful. For
example, you can prove "Suc undefined ~= undefined", but what good does that do?
You have to prove the "stronger property" you talk about.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Jan 11 2021 at 11:48):

From: Manuel Eberl <eberlm@in.tum.de>
For polymorphic functions, one can at least prove parametricity, which
(by some extra-logical meta argument) should imply that the function
does not produce any "undefined"s unless they were already present in
the input.

I don't think that is very applicable in your case though. And it might
not be any more useful than just going through the definitions by hand
and checking that they don't call any partial functions like "hd" (there
are not /that/ many operations that can crash in the standard code setup
for HOL, I think).

In any case, HOL is a logic, not a programming language. It doesn't have
any notion of "execution". I therefore think that anything you do inside
the logic will never be able to capture statements about what happens
during execution faithfully.

Even if your definition logically does not produce "undefined", even if
you prove that it always retuns "42", you could still have a code
equation somewhere that does something silly like "if undefined =
(undefined :: nat) then … else …" that crashes at run time. Or
non-termination.

I think the only way to get any real guarantees would be to have a
semantics of the target language (that you export your code into) and
then reason about execution with that. Or do the opposite: take an
implementation of your algorithm and prove it equivalent to the HOL
definition through some verification framework.

Something like a verified code generator that certifies termination and
exception-freedom would also work. I think Lars Hupel's verified code
generator to CakeML went into that direction, but I don't know if he
proved these properties. Plus it would probably not be able to handle an
example as big as yours is likely to be.

Manuel
smime.p7s

view this post on Zulip Email Gateway (Jan 11 2021 at 14:14):

From: David Kretzmer <david.k@posteo.de>
It is true that I'm currently using Isabelle/HOL with a mindset based on
executable programming languages, and in this context "undefined" feels
a bit like the danger of dereferencing an invalid pointer. However,
since the exceptional behavior of "undefined" is only part of the target
language it makes sense that you cannot reason about it in Isabelle/HOL.

Also, without code generation, I guess the only thing you care about a
(function) definition is what you can prove about it. If the property
you want to prove uses parts of the definition that unexpectedly depend
on "undefined", then the proof may fail and you have to fix the
definition. On the other hand, if "undefined" occurs only in parts of
the definition that are irrelevant for the proof, then you don't care.

So the difference between the proof language perspective and the
programming language perspective seems to be that in the former, you
deal with "undefined" when you encounter it (in this sense "undefined"
may just indicates an error in the definition, no different from other
possible definition errors), while in the programming language
perspective you want to ensure from the start that you never encounter
"undefined".

Anyway, thanks for the detailed responses!

view this post on Zulip Email Gateway (Jan 11 2021 at 14:21):

From: Lawrence Paulson <lp15@cam.ac.uk>
Perhaps it would work better if you formalised a more traditional operational semantics, making explicit the idea of an execution becoming stuck (due to either an error in the semantics or a runtime error). Presumably an evaluation function could be refined from that.

Larry

view this post on Zulip Email Gateway (Jan 11 2021 at 17:48):

From: David Kretzmer <david.k@posteo.de>
Do I understand correctly that by "more traditional" you mean defining
the semantics by a transition relation using, e.g., an inductive
predicate? Initially the semantics actually was defined using an
inductive predicate, and then "undefined" is indeed not a problem.
However, the semantics needs to detect and handle many different runtime
errors, which led to many similar but slightly different rules in the
transition relation. For me, defining the same semantics in a functional
style was more concise.


Last updated: Jul 15 2022 at 23:21 UTC