| 
|
QuoteRef: wulfWA6_1976
topics >
all references >
Topic:
state
Topic:
managing shared memory
Topic:
program proof via assertions
ThesaHelp:
references t-z
Topic:
function syntax definition
Topic:
notations for object access
Topic:
design for change
Topic:
separate a module's interface specification from its implementation
Topic:
information hiding
Topic:
primitive data type as memory
Topic:
primitive data types for Thesa
Topic:
data type as a set of operations
Topic:
initialized constants
Topic:
type parameter
Reference
Wulf, W.A., London, R.L., Shaw, M., "Abstraction and verification in Alphard: Introduction to language and methodology", University of Southern California, Information Sciences Institute, ISI/TR-76-46, June 1976. Google
4 ;;Quote: a modifiable program must retain the structure of its development
7 ;;Quote: Alphard was designed for its verification technique
9 ;;Quote: Alphard's specification sections are the user's sole source of information about a form QuoteRef: wulfWA6_1976 ;;9 specification consists of abstract invariant, required properties of parameters, initial value properties, input/output relations for each abstract operation QuoteRef: wulfWA6_1976 ;;9 Hoare '69: pre-condition (y) {operation} post-condition (y) QuoteRef: wulfWA6_1976 ;;10 Wulf's proof method: prove that abstract and concrete representations are consistent and the pre-post conditions hold across operations QuoteRef: wulfWA6_1976 ;;17 Alphard has unique and shared representations of a data type
18 ;;Quote: in Alphard, every function has concrete input and output assertions QuoteRef: wulfWA6_1976 ;;19 Alphard defines abstract states (eg empty stack) for describing different predicates QuoteRef: wulfWA6_1976 ;;20 ref by function (element, parameters) or element. function (params)
21 ;;Quote: the only primitive form of Alphard corresponds to untyped, computer memory
30 ;;Quote: Alphard's type declaration may include a list of necessary and sufficient operations
30 ;;Quote: Alphard allows initialized types; i.e., it is constant once defined
Topic: state (35 items)
Topic: managing shared memory (74 items)
Topic: program proof via assertions (61 items)
ThesaHelp: references t-z (309 items)
Topic: function syntax definition (17 items)
Topic: notations for object access (7 items)
Topic: design for change (75 items)
Topic: separate a module's interface specification from its implementation (86 items)
Topic: information hiding (50 items)
Topic: primitive data type as memory (29 items)
Topic: primitive data types for Thesa (82 items)
Topic: data type as a set of operations (38 items)
Topic: initialized constants (12 items)
Topic: type parameter (34 items)