Abstract
This document presents the formalization of an object-oriented data and store model in Isabelle/HOL. This model is being used in the Java Interactive Verification Environment, Jive.
GNU Lesser General Public License (LGPL)Topics
Theories of JiveDataStoreModel
- TypeIds
- JavaType
- DirectSubtypes
- Subtype
- Attributes
- AttributesIndep
- Value
- Location
- Store
- StoreProperties
- JML
- UnivSpec