Generating Cases from Labeled Subgoals

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. 1 

• Type: Journal
• Year: 2015
• Where: AFP
• Authors: Lars Noschinski
• Keywords: AFP 2015, Formal Methods