Generating Cases from Labeled Subgoals

 

Title: Generating Cases from Labeled Subgoals
Author: Lars Noschinski
Submission date: 2015-07-21
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.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.