MSc thesis in Applied Mathematics,
IST 1996.
Supervisors:
Prof. Amílcar Sernadas
and
Dr. Vasco Vasconcelos.
ABSTRACT
A fragment of the language GNOME for formal specification of concurrent, interactive and reactive systems is presented. It is an object-oriented language, class-based and object-based. A specification defines a community of objects for which an operational semantics is provided. To this end, an untyped calculus of concurrent objects --- TyCO --- with asynchronous communication and name-passing is introduced. TyCO has the favour of Pi-Calculus, Nu-Calculus and Process Algebras like CCS. The semantic map of the language GNOME into TyCO is defined. A GNOME class is represented by a TyCO agent and an object, instance of a class, is represented by a process, instance of an agent. A typing system for TyCO is also presented, similar to those of the Lambda-Calculus, but assigning types to names and typings (sets of name-type pairs) to processes. The type system provides partial specification as communication protocols for processes. Some of the most important properties of type system are shown, such as the subject-reduction, the absence of run-time errors in typable processes, the computability of the inference of types and typings and the decidability of the assigning of types and typings. It is discussed how to use the type system to prove partial-correctness of specifications regarding a certain type of invariance properties, concluding that it is not possible.