Email Gateway (Aug 22 2022 at 10:40): Email Gateway (Aug 22 2022 at 10:40):From: Tobias Nipkow <nipkow@in.tum.de>
Generating Cases from Labeled Subgoals
Lars Noschinski
Isabelle/Isar provides named cases to structure proofs. This article
contains an implementation of a proof method \texttt{casify}, which can
be used to easily extend proof tools with support for named cases. Such
a proof tool must produce labeled subgoals, which are then interpreted
by \texttt{casify}.
As examples, this work contains verification condition generators
producing named cases for three languages: The Hoare language from
\texttt{HOL/Library}, a monadic language for computations with failure
(inspired by the AutoCorres tool), and a language of conditional
expressions. These VCGs are demonstrated by a number of example programs.
http://afp.sourceforge.net/entries/Case_Labeling.shtml
Thank you, Lars!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC