Abstract: |
Isabelle/Isar provides named cases to structure proofs. This article
contains an implementation of a proof method 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 casify.
As examples, this work contains verification condition generators
producing named cases for three languages: The Hoare language from
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. |
BibTeX: |
@article{Case_Labeling-AFP,
author = {Lars Noschinski},
title = {Generating Cases from Labeled Subgoals},
journal = {Archive of Formal Proofs},
month = jul,
year = 2015,
note = {\url{http://isa-afp.org/entries/Case_Labeling.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|