DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
The Semantics of Ada Access Types (Pointers) in the State Delta Verification System (SVDS).
AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP
Pagination or Media Count:
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.
APPROVED FOR PUBLIC RELEASE