Larch : uma alternativa para especificação formal

Abstract

Pesquisas recentes na área de especificação são enfáticas no use pratico de especificações formais no projeto de programas. Uma maneira de satisfazer isto, e providenciando linguagens de especificação que sejam acessíveis simultaneamente a projetistas, a especificadores e a programadores. A abordagem Larch esta orientada a especificação de módulos de programas a serem implementados em uma linguagem de programação particular. Cada especificação Larch tem dois componentes: uma escrita em uma linguagem derivada de uma linguagem de programação, chamada Linguagem de Interface Larch; e outra escrita em uma linguagem comum e independente de qualquer linguagem de programação, chamada Linguagem Compartilhada Larch. Abstrações são formuladas na linguagem Compartilhada. As linguagens de Interface (orientadas a predicados) são usadas para descrever o comportamento de procedimentos. As descrições dadas nas linguagens de interface são dadas em termos destas abstrações e podem também incluir manipulações de erros, situações de exceção e limites de implementação. Este trabalho apresenta um estudo da família de linguagens Larch e uma aplicação das mesmas a um problema prático. Na primeira parte, faz-se uma descrição da Linguagem Compartilhada Larch (sintaxe, semântica, consistência, completeza, gramática, núcleo) a das linguagens de Interface Larch com exemplos orientados a linguagem de programação Pascal. Na segunda parte, apresenta - se a especificação do modelo relacional para banco de dados, também orientado a programadores em Pascal. O núcleo desta especificação esta contida em [GUT 85) e é um conjunto de módulos de relações e estruturas matemáticas. Depois segue a especificação de conjunto, lista, duas, relação e banco de dados relacional. Cada especificação, al6m das duas componentes já mencionadas tem uma parte de comentários que é utilizada somente para fins didáticos e entender melhor a especificação.

Recent research on the specification area is emphatic on the practical use of formal specifications in programs design. One way to satisfy this, is the supply of specification languages that could be accessible simultaneously to designers, specifiers and programmers. The Larch approach is geared towards specifying program modules to be implemented in particular programming languages. Each Larch specification has two components: one written in a language derived from a programming language, called Larch Interface Language; and another component written in a language independent of any programming language, called Larch Shared Language. Abstractions are formulated in the Shared Language. The Interface Language (predicate-oriented) is used to describe the intended behaviour of procedures. Descriptions given in the interface languages are given in terms of those abstractions and might also include error and exception handling situations and implementation limits. This work presents a study of the family of Larch Languages and their aplication to a practical problem. The first part is a description of Larch Shared Language (syntax, semantics, consistency, completeness, grammar, kernel) and Larch Interface Language with examples oriented to Pascal programming language. The second part presents the specification of the relational model for databse, also oriented to Pascal programmers. The kernel of this specification is taken from [GUT 85) and is a modules set of relations and mathematical structures. This is followed by specification of concept of set, list, tuple, relation and relational database. Each specification, besides the two component mentioned above, has a commentary used only for didactic purpose and to explain better the specification.