The Semantics of Ada Access Types (Pointers) in the State Delta Verification System (SVDS).
Abstract
We propose a method for handling Ada access types (pointers) in SDVS, i.e., a method that allows SDVS to translate and reason about Ada programs containing access types. The method is built upon "higher-order places", i.e., "places" that have other places as contents. We give the state delta semantics for various Ada constructs involving access types, discuss the theory and implementation of higher-order places, and give a partially worked example of an Ada program involving access types.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 30, 1992
- Accession Number
- ADA288815
Entities
People
- L. G. Marcus
Organizations
- The Aerospace Corporation