Formal Methods for Object-Based Computing

点击翻译按钮获取中文摘要

Objects are programming abstractions that encapsulate mutable internal state and provide operations to manipulate the state. Object-based computing is the programming paradigm that uses objects to structure the state-manipulation carried out in programs. The goal of this project is to develop formal methods for specifying, conceptualizing, and reasoning about object- based programs. These formal methods include: (1) Type systems: what kinds of semantic entities are involved in object-based programs, and how does one capture them in type systems for programming languages? (2) Denotational semantics: what mathematical abstractions are involved in capturing the bahaviors of object-based programs? (3) Specifications: How does one specify the behaviors of individual objects? (4) Reasoning methods: what methods are appropriate and useful for proving properties of object-based programs? The Direction being pursued is to build on the several decades of research in functional programming so as ato achieve a "tight integration" of programming concepts and mathmatical tools in working with object-based programs. Of primary focus are algebraic specification and equational reasoning techniques using lambda-calculus-based higher-order language frameworks. ***