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.
License
Topics
Session JiveDataStoreModel
- TypeIds
- JavaType
- DirectSubtypes
- Subtype
- Attributes
- AttributesIndep
- Value
- Location
- Store
- StoreProperties
- JML
- UnivSpec