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.

  author  = {Lars Noschinski},
  title   = {Generating Cases from Labeled Subgoals},
  journal = {Archive of Formal Proofs},
  month   = jul,
  year    = 2015,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Used by: Planarity_Certificates