Object-oriented programminglanguages allow inter-object aliasing. Although necessary to construct linked data structures and networks of interacting objects, aliasing is problematic in that an aggregate object's ...
详细信息
ISBN:
(纸本)9781581130058
Object-oriented programminglanguages allow inter-object aliasing. Although necessary to construct linked data structures and networks of interacting objects, aliasing is problematic in that an aggregate object's state can change via an alias to one of its components, without the aggregate being aware of any *** types form a static type system that indicates object ownership. This provides a flexible mechanism to limit the visibility of object references and restrict access paths to objects, thus controlling a system's dynamic topology. The type system is shown to be sound, and the specific aliasing properties that a system's object graph satisfies are formulated and proven invariant for well-typed programs.
The first version of Gypsy was introduced in 1976 to support the specification and construction of verified programs. A second version has evolved based on the experiences of the last two years. The changes introduced...
详细信息
ISBN:
(纸本)9780897910002
The first version of Gypsy was introduced in 1976 to support the specification and construction of verified programs. A second version has evolved based on the experiences of the last two years. The changes introduced in the second version are described. Some experiences with the specification and proof methodology are discussed, and the status of the implementation of the Gypsy compiler and verification system is summarized.
In Expressions of Change modifications to programs replace text files as the primary building blocks of software development. This novel approach yields structured historic information at arbitrary levels of program g...
详细信息
ISBN:
(纸本)9782955747421
In Expressions of Change modifications to programs replace text files as the primary building blocks of software development. This novel approach yields structured historic information at arbitrary levels of program granularity across the programming toolchain. In this paper the associated questions of programming language design are explored. We do so in the context of s-expressions, creating a modification-based infrastructure for languages in the Lisp family. We provide a framework for evaluation of the relative utility of different formalizations of program construction, which consists of the following: first, a requirement for completeness, meaning that a formalization of program construction should allow for the transformation of any valid program into any other. Second, a preference for succinctness over verbosity; succinctness of both of the formalization itself and typical expressions in the formalization. Third, a measure of the ability to clearly express intent. Fourth, a description of three ways in which the means of combination of the program itself and those of its means of construction may interact. Finally, we give a particular example of a formalization and use the provided framework to establish its utility.
In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of math...
详细信息
The designer of a computing system should adopt explicit criteria for accepting or rejecting proposed system features. Three possible criteria af this kind are input recordability, input specifiability, and asynchrono...
详细信息
The designer of a computing system should adopt explicit criteria for accepting or rejecting proposed system features. Three possible criteria af this kind are input recordability, input specifiability, and asynchronous reproducibility of output. These criteria imply that a user can, if he desires, either know or control all the influences affecting the content and extent of his computer's output. To define the scope of the criteria, the notion of an abstract machine of a programminglanguage and the notion of a virtual computer are explained. Examples of applications of the criteria concern the reading of a time-of-day clock, the synchronization of parallel processes, protection in multipragrammed systems, and the assignment of capability indexes. [ABSTRACT FROM AUTHOR]
暂无评论