Generating Cases from Labeled Subgoals

3 years 8 months ago
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
Lars Noschinski
Added 13 Apr 2016
Updated 13 Apr 2016
Type Journal
Year 2015
Where AFP
Authors Lars Noschinski
Comments (0)