Universidade Federal de Minas Gerais
Instituto de Ci^encias Exatas
Departamento de Ci^encia da Computaca~o
Laboratorio de Linguagens de Programac~ao
Machna: A Linguagem de Especicac~ao de ASM
by
Fabio Tirelo
Roberto da Silva Bigonha
Marcelo de Almeida Maia Vladimir Oliveira di Iorio
LLP 008/99
Caixa Postal, 702
30.161-970 { Belo Horizonte
Minas Gerais { Brazil
August, 1999
Resumo
Este texto contem a denic~ao da Linguagem de Programac~ao Machna, que e uma linguagem
baseada no paradigma de Programac~ao Algebrica, derivado do modelo de Maquinas de Estado
Abstratas (ASM). Nesta denic~ao, apresentamos a sem^antica informal de Machna, descrevendo
os aspectos sem^anticos da linguagem por meio de linguagem natural e exemplos de utilizaca~o
das construc~oes da linguagem. Ao nal, apresentamos varios exemplos de programas escritos em
Machna.
Sumario
1 A Linguagem Machna
1.1
1.2
1.3
1.4
1.5
1.6
1.7
1.8
1.9
1.10
1.11
1.12
1.13
1.14
1.15
1.16
1.17
1.18
1.19
1.20
1.21
Introduc~ao . . . . . . . . . . . . . . . . . . .
Comentarios . . . . . . . . . . . . . . . . . .
Literais . . . . . . . . . . . . . . . . . . . .
Palavras Reservadas . . . . . . . . . . . . .
Identicadores . . . . . . . . . . . . . . . .
Notac~ao Para Sintaxe . . . . . . . . . . . .
Uma Especicac~ao em Machna . . . . . . .
Modulos . . . . . . . . . . . . . . . . . . . .
Agentes . . . . . . . . . . . . . . . . . . . .
Termino da Execuc~ao . . . . . . . . . . . .
Mecanismos de Visibilidade . . . . . . . . .
Declarac~ao de Tipos . . . . . . . . . . . . .
1.12.1 Enumerac~oes . . . . . . . . . . . . .
1.12.2 Uni~oes Disjuntas . . . . . . . . . . .
1.12.3 Tipo ? . . . . . . . . . . . . . . . . .
1.12.4 Intervalos . . . . . . . . . . . . . . .
1.12.5 Tuplas . . . . . . . . . . . . . . . . .
1.12.6 Conjuntos . . . . . . . . . . . . . . .
1.12.7 Listas . . . . . . . . . . . . . . . . .
1.12.8 Tipos Funcionais . . . . . . . . . . .
1.12.9 Tipos Agentes . . . . . . . . . . . .
1.12.10Denic~oes de Tipos . . . . . . . . . .
Regras de Visibilidade para Tipos . . . . .
Regras para Deduc~ao de Tipos . . . . . . .
Equival^encia de Tipos . . . . . . . . . . . .
Compatibilidade de Tipos . . . . . . . . . .
Declarac~ao de Func~oes . . . . . . . . . . . .
Declarac~ao de Func~oes Externas . . . . . .
Denic~ao das Regras de Inicializac~ao . . . .
Declarac~ao de Abstrac~oes de Regras . . . .
Sec~ao de Denic~ao de Regras de Transic~ao .
1.21.1 Regras Basicas . . . . . . . . . . . .
i
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1
1
1
1
2
2
2
2
3
4
5
6
7
7
8
8
8
8
8
8
9
9
9
9
10
11
11
12
12
13
14
14
14
1.21.2 Regra forall . . . . . . . . . . . . . . . . . . . .
1.21.3 Regra choose . . . . . . . . . . . . . . . . . . .
1.21.4 Regras Para Criac~ao e Eliminac~ao de Agentes .
1.21.5 Regra Para Parada . . . . . . . . . . . . . . . .
1.21.6 Regra let . . . . . . . . . . . . . . . . . . . . .
1.21.7 Regra case . . . . . . . . . . . . . . . . . . . .
1.21.8 Regra with . . . . . . . . . . . . . . . . . . . .
1.21.9 Regra de Chamada a Ac~oes . . . . . . . . . . .
1.22 Invariante da Execuc~ao . . . . . . . . . . . . . . . . .
1.23 Sintaxe de Express~oes . . . . . . . . . . . . . . . . . .
1.23.1 Operadores de Machna . . . . . . . . . . . . .
1.23.2 Valores Booleanos . . . . . . . . . . . . . . . .
1.23.3 Caracteres . . . . . . . . . . . . . . . . . . . . .
1.23.4 Numeros Inteiros . . . . . . . . . . . . . . . . .
1.23.5 Numeros Reais . . . . . . . . . . . . . . . . . .
1.23.6 Cadeias de Caracteres . . . . . . . . . . . . . .
1.23.7 Aplicac~ao de Func~oes . . . . . . . . . . . . . .
1.23.8 Listas . . . . . . . . . . . . . . . . . . . . . . .
1.23.9 Conjuntos . . . . . . . . . . . . . . . . . . . . .
1.23.10Tuplas . . . . . . . . . . . . . . . . . . . . . . .
1.23.11Mapeamentos . . . . . . . . . . . . . . . . . . .
1.23.12Convers~ao de Tipos . . . . . . . . . . . . . . .
1.23.13Condicionais e Let . . . . . . . . . . . . . . . .
1.23.14Express~oes Especiais . . . . . . . . . . . . . . .
1.23.15Gramatica das Express~oes . . . . . . . . . . . .
1.24 Manipulac~ao de Arquivos . . . . . . . . . . . . . . . .
2 Exemplos
2.1
2.2
2.3
2.4
Pesquisa Binaria . . . . . . . . . . . . . . . .
Ordenac~ao por Selec~ao . . . . . . . . . . . . .
Numeros Primos . . . . . . . . . . . . . . . .
Especicac~ao da Sem^antica de Tiny . . . . .
2.4.1 Modulo de Globais (Globals) . . . . .
2.4.2 Modulo de Operac~oes (Operations) .
2.4.3 Modulo de Express~oes (Expressions)
2.4.4 Modulo de Comandos (Comandos) . .
2.4.5 Modulo principal (Tiny) . . . . . . . .
2.4.6 Disparo do Agente de Execuc~ao . . . .
2.5 Jantar dos Filosofos . . . . . . . . . . . . . .
ii
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
15
16
16
17
17
18
18
19
19
19
19
20
20
20
21
21
22
22
22
23
23
24
25
25
26
26
29
29
30
30
31
31
32
33
34
35
35
36
Cap
tulo 1
A Linguagem Machna
1.1 Introduc~ao
Neste captulo, apresentamos a linguagem Machna, que e baseada na metodologia de Maquinas
de Estado Abstratas (ASM), com suporte a modularidade, tipos e construc~oes de alto nvel. Um
programa em Machna tem o estilo de Programac~ao Algebrica, isto e, o estado da computac~ao
e descrito por uma algebra e existe uma regra de transica~o que promove a mudanca de estados.
Desta forma, a escrita de um programa algebrico consiste em denir:
um vocabulario, que e o conjunto de smbolos da especicac~ao, isto e, o conjunto dos identicadores e operadores conhecidos;
uma algebra inicial, que e a interpretac~ao inicial do vocabulario;
uma regra de transic~ao, que promove a transic~ao de estados (algebras).
1.2 Comentarios
Comentarios em Machna podem ser de dois tipos:
um texto que se inicia com /* e termina com */, podendo haver aninhamento;
um texto que se inicia com // e vai ate o m da linha.
1.3 Literais
Os literais de Machna s~ao:
caracteres do conjunto ASCII, representados por um smbolo entre apostrofos, p.ex.
'5' e
ou por um codigo denotando caracteres especiais, como '\n', '\0', etc.
numeros inteiros { numeros inteiros podem ser escritos em decimal (sequ^encia de dgitos),
octal (0 seguido de sequ^encia de dgitos de 0 a 7) ou em hexadecimal (0x seguido de
sequ^encia de dgitos ou letras de A a F ou a a f). Os numeros inteiros est~ao no intervalo [-2147483648,2147483647].
numeros de ponto utuante { sequ^encia de dgitos, seguida por uma parte fracionaria
opcional, seguida por uma parte de expoente opcional; a parte fracionaria consiste em
um ponto (".") seguido por uma sequ^encia de dgitos; a parte do expoente consiste em
'a',
1
ou E, seguido por um sinal opcional (+ ou -), seguido por uma sequ^encia de dgitos.
Numeros de ponto utuante t^em valor maximo 1.79769313486231570E+308 e valor mnimo
4.94065645841246544E-324, seguindo o padr~ao IEEE 754 para ponto utuante.
cadeias de caracteres { sequ^encia de caracteres entre aspas, como por exemplo, "string",
"isto e\' um teste", "fim de linha\n", etc.;
e
1.4 Palavras Reservadas
As palavras reservadas de Machna s~ao:
action
choose
dynamic
external
in
list
of
self
transition
algebra
create
else
false
init
machina
or
set
true
and
default
elseif
forall
interleaved
module
otherwise
static
type
as
derived
end
if
is
nil
public
stop
with
case
do
enum
import
let
not
satisfying
then
1.5 Identicadores
Identicadores em Machna s~ao divididos em dois tipos:
identicadores de tipos e modulos { formados por uma ou mais letras, onde a primeira e
maiuscula;
identicadores de variaveis { formado por uma ou mais letras, onde a primeira e minuscula;
podem ser decoradas, isto e, terminadas, com numeros;
1.6 Notac~ao Para Sintaxe
Para descric~ao da gramatica, utilizaremos a BNF estendida [?], ou XBNF. As construc~oes utilizadas s~ao semelhantes a BNF, com as seguintes extens~oes:
j Opc~oes
f X g Zero ou mais ocorr^encias de X
[X]
Zero ou uma ocorr^encia de X
Os caracteres que representam meta-smbolos, se utilizados na gramatica, ser~ao escritos em aspas,
como por exemplo \f".
1.7 Uma Especicac~ao em Machna
Uma especicac~ao em Machna consiste em uma coleca~o de um ou mais modulos, denominados
modulos de programa, ou somente modulos. Associado a uma especicac~ao, pode haver uma ou
mais \denic~oes de maquina", na qual denimos e disparamos os agentes que executam as regras
dos modulos.
2
1.8 Modulos
Um modulo especica um nome para o programa de um agente, a regra que este agente executa, e
sua algebra subjacente, isto e, smbolos, universos e interpretac~ao dos smbolos. Um modulo tem
a forma:
module nome-modulo
import:
elementos importados
algebra:
algebra subjacente { tipos, funco~es, ac~oes, inicializac~oes
transition:
regra de transic~ao
end
Uma denic~ao de maquina especica o seu nome e possui uma sec~ao de inicializac~oes, onde s~ao os
agentes criados e disparados. Cada denica~o possui a seguinte forma:
machina nome-maquina
end
declarac~oes do ambiente de execuca~o
inicializac~oes { criac~ao dos agentes
Modulos possuem tr^es partes:
Importaco~es { dene os modulos que ser~ao importados (Sec~ao 1.11);
A lgebra { dene a algebra subjacente ao modelo, contendo os sorts ou tipos, as func~oes, as
ac~oes e as regras de inicializac~ao;
Regra de transic~ao { dene a regra de transic~ao do modulo, isto e, o programa dos agentes.
A sec~ao de algebra e divida nas seguintes subseco~es:
Denic~ao de tipos { dene tipos (sorts) de dados que ser~ao utilizados na especicac~ao
(Sec~ao 1.12);
Func~oes { agrupa as denic~oes de func~oes por classe, podendo ser estatica, din^amica e derivada. Por exemplo, uma declarac~ao da forma
static
f := ...
g := ...
h := ...
dynamic
a := ...
b := ...
dene f, g e h como func~oes estaticas, e a e b como din^amicas (Sec~ao 1.17);
Func~oes externas { dene os cabecalhos das func~oes externas (Sec~ao 1.18);
Aco~es { dene as transic~oes parametrizadas, que s~ao abstrac~oes de regras de transic~ao
(Sec~ao 1.20);
Inicializac~oes { regra de inicializac~ao de func~oes din^amicas e denic~ao de func~oes estaticas
(Sec~ao 1.19);
3
A sintaxe de um modulo e a seguinte:
module
module-body
import-part
algebra-part
transition-part
invariant-part
module-import
imported-list
imported-element
algebra-section
type-section
type-pdecl
function-section
class-modier
function-pdecl
external-section
external-pdecl
action-section
action-pdecl
init-section
::=
::=
::=
::=
::=
::=
::=
::=
::=
::=
module module-name module-body end
[import-part] [algebra-part] [transition-part] [invariant-part]
import: module-import f , module-import g
algebra: f algebra-section g
[interleaved] transition: transition-rule
invariant: expression
module-name [imported-list]
( imported-element f , imported-element g )
id j type-name
type-section
function-section
external-section
action-section
init-section
::= type type-pdecl f ; type-pdecl g
::= [public] type-declaration
::= class-modier function-pdecl f ; function-pdecl g
::= static j dynamic j derived
::= [public] function-declaration
::= external external-pdecl f ; external-pdecl g
::= [public] external-declaration
::= action action-pdecl f ; action-pdecl g
::= [public] action-declaration
::= init transition-rule
j
j
j
j
1.9 Agentes
A cada modulo pode ser associado um conjunto de agentes, que executam a sua regra. Agentes
s~ao criados por meio de uma regra especial de nome create, como sera visto na Sec~ao 1.21.
A regra de transic~ao de um modulo declarada como interleaved e executada repetidamente de
forma entremeada com a de outras regras. Apos cada transic~ao, o controle volta para o modulo
maquina, que pode livremente escalar o proximo agente a prosseguir em execuc~ao. Transic~oes que
n~ao s~ao declaradas como interleaved s~ao executadas repetidamente ate o seu termino.
Agentes podem ser referenciados, de dentro de um programa, por meio de func~oes, assim como
qualquer valor. Para isto, s~ao denidos em Machna o tipo Agent e o construtor de tipos agent
of M, onde M e um nome de modulo. O tipo agent of M e o conjunto de agentes que executam a
regra do modulo M. Mais detalhes sobre este tipo ser~ao mostrados na Sec~ao 1.12.9.
Todo agente possui uma func~ao especial de nome self 2 agent of M, que retorna a sua identicac~ao, onde M e o modulo que contem a regra que o agente executa. Desta forma, representamos
informac~oes locais a um agente.
Uma maquina deve denir a criac~ao dos agentes que iniciar~ao a execuc~ao. Considere, por exemplo,
a denica~o dos modulos e a criac~ao dos agentes dada por:
machina D
module C
module B
module A
create a : agent of A
decls of C
decls of B
decls of A
create b : agent of B
transition: transition: transition:
create c : agent of C
rule of C
rule of B
rule of A
end
end
end
end
A relac~ao entre os agentes denidos na machina D e os modulos A, B e C pode ser vista na
Figura 1.1.
4
decls-A
a
rule-A
decls-B
b
rule-B
decls-C
c
rule-C
Figura 1.1: Exemplo de espaco de declarac~oes e regras e acesso de agentes.
Na Sec~ao 1.11, mostraremos como estender este modelo para lidar com o compartilhamento de
declarac~oes entre modulos.
1.10 Termino da Execuc~ao
A execuc~ao termina com a execuc~ao do comando stop, ou quando a guarda principal n~ao for
verdadeira. Por exemplo, a execuc~ao da especicac~ao abaixo so terminara com a execuc~ao do
comando stop.
module A
...
transition:
if cond-parada then
stop
else
...
end
end
Se todas as guardas do programa avaliarem em falso, ent~ao a execuc~ao terminara. Entretanto, se
houver alguma chamada a func~ao externa nas guardas, a execuc~ao cara suspensa, esperando que
a func~ao externa seja modicada e alguma guarda se torne verdadeira.
module B
external f : Int;
dynamic g(x : Int)
transition:
if f = 10 then
g(10) := 0
else
g(10) := 1
end
end
:
Int;
Quando a regra for executada a primeira vez, se o valor da funca~o externa f for 10, o valor de
g no ponto 10 sera atualizado para 0. Enquanto o valor de f n~ao mudar, a regra g(10) := 0
5
sera executada, o que n~ao causara mudanca alguma no estado. Neste caso, a execuc~ao n~ao sera
abortada, pois n~ao sabemos se no proximo estado, o valor da func~ao externa sera diferente de 10.
1.11 Mecanismos de Visibilidade
Um modulo pode importar os elementos (declarac~oes de func~oes, tipos e ac~oes) de outros modulos.
Toda declarac~ao e privada a um modulo, isto e, visvel somente dentro do modulo no qual foi feita.
Um elemento so n~ao e privado a um modulo se for explicitamente declarado como publico, por
meio do modicador de visibilidade public.
Os elementos publicos de um modulo M1 tornam-se visveis dentro de outro modulo M2, quando
M1 for importado em M2. Isto e feito na parte de importac~oes do modulo M2, de uma das
seguintes maneiras:
import:
import:
M1
M1(a,b)
Torna visveis todos os elementos publicos de M1
Torna visveis somente os elementos publicos a e b de M1
Da primeira maneira, todos os elementos publicos de M1 s~ao visveis dentro de M2. Um elemento
a, p
ublico de M1 e acessado em M2 da forma M1.a. Da segunda maneira, os elementos a e b de
M1 s~
ao diretamente visveis em M2, n~ao sendo necessaria a qualicac~ao do modulo para acessar a
ou b, isto e, estes identicadores podem ser acessados diretamente em M2, sem a necessidade de
especicar o modulo a que pertencem.
Por exemplo, considere os modulos abaixo:
module X
public a;
b
...
end
module Y
import: X;
public m,n;
... X.a ...
end
module Z
import:
...
...
end
X, Y(n);
X.a ...
n ...
O modulo X dene um elemento de nome a, que e visvel a partir de outros modulos, enquanto a
declarac~ao de b e visvel somente dentro de X, isto e, e privada a este modulo. A linha import
X, no m
odulo Y, importa todos os elementos publicos de X, o que signica que o elemento a, em
X, e visvel dentro de Y, sob o nome de X.A. Da mesma maneira, a e visvel no modulo Z, sendo
necessaria a qualicac~ao do modulo, assim como no modulo Y. Entretanto, como a importac~ao
do modulo Y em Z explicitou quais identicadores s~ao visveis, podemos utilizar o nome n em Z
diretamente, sem a necessidade de escrever Y.n. Alem disso, observe que o nome m, denido como
publico em Y tambem e visvel em Z, mas requer completa qualicac~ao, pois n~ao foi explicitado
na importac~ao.
E importante ressaltar, ainda, que a clausula import n~ao causa a duplicac~ao de declarac~oes; ela
apenas torna as declarac~oes publicas de um modulo visveis a outros modulos.
Na Figura 1.2, ilustramos como os agentes que executam a regra denida em um modulo acessam
as declarac~oes visveis do exemplo abaixo.
module A
module B
module C
D
public ax; public bx; public cx; machina
create a
ay;
by;
cy;
create b
transition: transition: transition:
create c
rule of A
rule of B
rule of C
end
end
end
end
6
:
:
:
agent of
agent of
agent of
A
B
C
ax
a
rule-A
b
rule-B
c
rule-C
ay
bx
by
cx
cy
Figura 1.2: Exemplo de Visibilidade entre Modulos. Linhas pontilhadas ligando agentes a declarac~oes signicam que o agente pode acessar a declarac~ao e linhas n~ao-tracejadas ligando agentes
a regras mostra qual regra de transic~ao o agente esta executando.
1.12 Declarac~ao de Tipos
Os tipos (ou sorts) primitivos de Machna s~ao Bool, Char, Int, Real e String, Set, List, ?.
Os tipos estruturados, isto e, formados por meio de geradores de tipos s~ao:
enumeraca~o de valores;
tupla de elementos;
conjunto de um dado tipo;
lista de um dado tipo;
tipo funcional (n~ao permitindo func~oes de ordem mais alta);
uni~ao disjunta;
Um nome de tipo e uma sequ^encia de letras, onde a primeira letra e maiuscula.
O tipo () (null) e utilizado em denic~oes de tipos recursivos.
1.12.1 Enumerac~oes
Tipos enumerados s~ao denidos por meio de enumerac~ao de identicadores, como no exemplo
abaixo:
RGBColor
is enum f
red, green, blue
g:
Enumerac~oes diferentes devem denir identicadores diferentes. Isto signica que n~ao e permitida
uma sequ^encia de declarac~oes da forma:
...
enum A is f
enum B is f
...
g
a, b, c
a, e, i, o, u
g
pois o identicador a esta sendo denido em duas enumerac~oes diferentes.
7
1.12.2 Uni~oes Disjuntas
Uma uni~ao disjunta e feita em Machna utilizando o operador \j". Por exemplo, o tipo Numero
abaixo e a uni~ao disjunta entre Int e Real:
is
Numero
:
Int | Real
Observac~ao: em uma uni~ao disjunta, os tipos componentes n~ao podem ser equivalentes.
1.12.3 Tipo ?
O tipo ? e denido como a uni~ao disjunta de todos os tipos possveis, com o valor default igual
a undef. Isto signica que, se x e do tipo ?, ent~ao x pode receber valores de quaisquer tipos. O
tipo ? so possui as operac~oes de atribuic~ao e comparac~ao por = ou !=. Convers~ao para o tipo real
do valor armazenado deve ser feita via comandos ou express~oes with e is.
1.12.4 Intervalos
Uma denic~ao de intervalo e feita como no exemplo:
UmACem
is
1..100
As express~oes que determinam os limites inferior e superior do intervalo devem ser manifestas e
seus tipos devem ser iguais e discretos.
1.12.5 Tuplas
As tuplas devem ser rotuladas. Pode-se utilizar a tupla vazia, (), em denic~oes de tipos recursivos.
Por exemplo, considere a declarac~ao:
Tree
is
:
() | (info:Info;left,right:Tree)
1.12.6 Conjuntos
O construtor de tipos \set of" e utilizado para denotar o tipo conjunto de elementos de um mesmo
tipo. Por exemplo
is set of
Intset
Int
e um tipo cujos elementos s~ao conjuntos de numeros inteiros. O tipo pre-denido Set e denido
como
Set
is set of ?:
Isto signica que Set e um conjunto generico, onde seus elementos n~ao precisam de ser do mesmo
tipo. As regras para utilizac~ao do tipo Set s~ao vistas na Sec~ao 1.23.9.
1.12.7 Listas
O construtor de tipos \list of" e utilizado para denotar o tipo lista de elementos de um mesmo
tipo. Por exemplo,
Intlist
is list of
Int
e um tipo cujos elementos s~ao listas de inteiros. Assim como em conjuntos, o tipo pre-denido
List e denido como:
List
is list of ?:
Desta forma, List representa uma lista generica, onde seus elementos n~ao precisam de ser do
mesmo tipo. As regras para utilizac~ao do tipo List s~ao vistas na Sec~ao 1.23.8.
8
1.12.8 Tipos Funcionais
O tipo funcional, cujo construtor e \->", e um tipo cujos valores s~ao func~oes entre domnios dados.
Por exemplo, o tipo Transition denido abaixo e uma func~ao de State Element em State:
Transition
is
:
(State,Element) -> State
N~ao e permitida a denic~ao de func~oes de ordem mais alta.
1.12.9 Tipos Agentes
O construtor de tipos agent of M e utilizado para denotar o tipo dos agentes que executam a
regra do modulo M. Existe tambem o tipo pre-denido Agent, que representa agentes de quaisquer
tipos. As operac~oes que podem ser feitas sobre agentes s~ao a criac~ao (Sec~ao 1.21.4), a eliminac~ao
(Sec~ao 1.21.4), a atribuic~ao, a passagem como par^ametro, o retorno de func~ao e a comparac~ao por
igualdade e diferenca.
1.12.10 Denic~oes de Tipos
Para permitir a escrita de tipos mutuamente recursivos, Machna permite que, na declarac~ao de um
tipo, possam aparecer nomes de tipos que ainda n~ao foram declarados. Entretanto, na denic~ao
de uma func~ao, os tipos utilizados devem estar completamente denidos.
Em uma denic~ao de tipos, pode haver tambem uma clausula default, que permite estabelecer o
valor default para inicializac~ao automatica de func~oes do tipo dado.
Uma sec~ao de declarac~ao de tipos tem a seguinte sintaxe:
type-declaration ::= type-id is type-expression [default expression]
type-expression ::= ()
j ?
j type-name
j [public] enum \f"id f , id g \g"
j type-expression \j" type-expression
j expression .. expression
j [public] ( tuple-element f ; tuple-element g )
j set of type-expression
j list of type-expression
j le of type-expression
j agent of type-expression
j type-expression -> type-expression
tuple-element
::= [public] id f , id g [: type-expression]
type-name
::= Bool j Char j Int j Real j String j List j Set
j Agent j InputStream j OutputStream j type-id
1.13 Regras de Visibilidade para Tipos
Quando um tipo declarado como publico e importado, o seu nome se torna visvel no ponto
de importac~ao, mas n~ao a sua estrutura. Entretanto, para os tipos tupla e enumerac~ao, pode
ser necessaria a exportac~ao da estrutura. Para isso, Machna dene as seguintes regras para
exportac~ao de estrutura:
Para exportar os elementos de uma enumerac~ao, escreve-se a palavra-chave public antes da
palavra enum. Por exemplo, no codigo abaixo, s~ao visveis externamente os nomes de A, B,
x, y, z,
ao passo que os nomes a, b e c n~ao s~ao visveis, pois pertencem a uma enumerac~ao
n~ao-publica.
9
type
public A is enum fa,b,cg;
public B is public enum fx,y,zg;
Para exportar um campo de uma tupla, escreve-se a palavra chave public antes do nome do
campo. A palavra chave public antes de uma lista de identicadores separados por vrgula
torna publico todos os identicadores da lista. Para tornar publicos todos os campos da
tupla, pode-se utilizar o modicador public antes da express~ao de tipo. Por exemplo, no
codigo abaixo, s~ao visveis externamente os identicadores A, B, C, b, e, f, m, n e p, ao passo
que os nomes x, y, z, a, c e d s~ao privados ao modulo.
type
public A is (x:Int;y,z:Real);
public B is (a:Int; public b:Real;
public C is public (m,n:A; p:B)
c,d:Bool;
public
e,f:Char);
1.14 Regras para Deduc~ao de Tipos
Machna possui as seguintes convenc~oes para deduc~ao de tipos:
nomes de tipos s~ao uma sequ^encia de letras, sendo que a primeira letra e sempre maiuscula;
nomes de func~oes, que aparecem em declarac~oes com especicac~ao de tipos, s~ao uma sequ^encia de letras, onde o primeiro caractere e sempre uma letra minuscula;
se o tipo de um identicador for explicitado na declarac~ao, como em a:X, ent~ao o tipo do
identicador e o tipo dado e o nome do identicador n~ao pode conter decoraca~o;
se o tipo n~ao for explicitado na declaraca~o, ent~ao as seguintes regras s~ao utilizadas para
determinac~ao do tipo:
{ nomes de func~oes e variaveis que cont^em decorac~oes (numeros no nal) possuem o
mesmo tipo da func~ao ou variavel sem a decorac~ao; por exemplo, os identicadores x1
e x2 t^em o mesmo tipo de x;
{ se o tipo do identicador sem decorac~ao n~ao foi declarado, capitaliza-se a primeira letra
do nome do identicador; se houver algum tipo com este nome, ent~ao este e o tipo do
identicador;
{ caso contrario, o tipo do identicador sera ?.
Por exemplo, considere a sequ^encia de declarac~oes abaixo:
...
A
...; // Declara
ca
~o do tipo A
X
...; // Declara
ca
~o do tipo X
Y
Int; // Declara
ca
~o do tipo Y
a,b,c:X; // Todas possuem o tipo X
x; // O tipo de x e X
y := 1; // O tipo de y e Int
z; // O tipo de z e ?
...
is
is
is
10
1.15 Equival^encia de Tipos
Em Machna, tudo que diz respeito a tipos e decidido em tempo de compilac~ao, de modo que,
a menos das express~oes de convers~ao, os objetos n~ao levam para a execuc~ao informac~oes sobre
os seus tipos. A disciplina de tipos de Machna e a equival^encia estrutural, denida da seguinte
maneira:
Dois tipos A e B s~ao equivalentes se e somente se uma das seguintes condic~oes abaixo se aplicarem:
A e B s~ao nomes de tipos id^enticos;
A e B s~ao nomes de tipos distintos, mas cada um e a refer^encia recursiva para a denic~ao de
tipo reexivo que ocorre exatametne na mesma posic~ao correspondente nas suas estruturas
de tipos;
A e B s~ao o tipo ? de uni~ao disjunta de todos os tipos;
A e B s~ao nomes de tipos distintos, cujas denic~oes visveis s~ao, respectivamente, as cadeias
mais longas AisA1 isA2 is:::isAn e B isB1 isB2 is:::isBm , tal que Ai , para 1 i n, Bj ,
1 j n s~ao nomes de tipos, e An e Bm s~ao os primeiros e unicos nomes repetidos em suas
respectivas cadeias;
B e uma express~ao de tipos e A e um nome de tipos, cuja denic~ao visvel e tal que Aisd ou
AisA1 isA2 is:::isAn isd, onde Ai , para 1 i n, s~ao nomes de tipos, e a express~ao de tipos
d e equivalente a express~ao de tipos B ;
A e uma express~ao de tipos e B e um nome de tipos, cuja denic~ao visvel e tal que B isd ou
B isB1 isB2 is:::isBn isd, onde Bi , para 1 i n, s~ao nomes de tipos, e a express~ao de tipos
d e equivalente a express~ao de tipos A;
A e B s~ao domnios de listas, A e da forma list of A1 e B e da forma list of B1 , e A1 e
equivalente a B1 ;
A e B s~ao o tipo polimorco de listas vazias;
A e B s~ao domnios de tuplas, A e da forma (A1 ; :::; An ), B e da forma (B1 ; :::; Bn ) e, para
1 i n, Ai e equivalente a Bi ; nomes de campos n~ao s~ao relevantes para a determinac~ao
da equival^encia;
A e B s~ao uni~oes disjuntas, A e da forma A1 j:::jAn , B e da forma B1 j:::jBn e, para 1 i n,
Ai e equivalente a Bi ;
A e B s~ao tipos funcionais, A e da forma A1 ->A2 , B e da forma B1 ->B2 , A1 e equivalente
a B1 e A2 e equivalente a B2 .
1.16 Compatibilidade de Tipos
Dizemos que um tipo A e compatvel com um tipo B , se uma express~ao do tipo A puder ser usada
em um lugar onde e esperada uma express~ao do tipo B . Por exemplo, se denimos que x e do
tipo A e y e do tipo B , a atribuic~ao x := y so e possvel se A for compatvel com B .
A regra de compatibilidade de Machna e a seguinte: um tipo A e compatvel com um tipo B se
e somente se A e B forem equivalentes ou B e uma uni~ao disjunta de tipos, da qual A e um dos
componentes. Por exemplo, nos casos abaixo, A e sempre compatvel com B :
A
A
A
is
is
is
(a,b:Int); B
...; B
...
...; B
?;
is
is
is (x,y:Int);
j A j ...;
11
Os casos especiais de compatibilidade s~ao relativos aos tipos genericos. Supondo que T e um tipo
qualquer e M e um nome de modulo, as regras de compatibilidade para estes tipos s~ao as seguintes:
O tipo list of T e compatvel com List;
O tipo set of T e compatvel com Set;
O tipo agent of M e compatvel com Agent.
1.17 Declarac~ao de Func~oes
As func~oes em Machna podem ser:
estaticas { s~ao as que n~ao podem sofrer atualizac~oes e nem acessar func~oes din^amicas ou
externas;
din^amicas { s~ao as que podem sofrer atualizac~oes;
derivadas { s~ao func~oes que n~ao podem sofre atualizac~oes, mas podem acessar func~oes
din^amicas ou externas;
externas { s~ao func~oes denidas e atualizadas no ambiente externo.
A classe da func~ao depende da sec~ao onde ela foi declarada. Por exemplo, uma func~ao estatica
deve ser declarada na sec~ao static. O corpo de uma func~ao estatica ou derivada pode ser denido
tanto na sec~ao de declarac~oes quanto na seca~o init (Sec~ao 1.19).
O ambiente de avaliac~ao do corpo de func~oes estaticas e formado pelas outras func~oes estaticas
ja denidas e pelos seus par^ametros. Func~oes externas ou din^amicas n~ao podem ser chamadas a
partir do corpo de uma func~ao estatica.
O nome da func~ao pode servir para determinar o tipo de retorno da func~ao, caso ele n~ao seja
explicitado, como mostrado na Seca~o 1.14. Da mesma forma, o nome de um par^ametro pode
servir para determinar o seu tipo. Quando o tipo de algum elemento n~ao e especicado e o
compilador n~ao conseguir deduzi-lo a partir de sua denic~ao, o seu tipo sera \?".
Abaixo, mostramos a sintaxe de denic~ao de func~oes e relac~oes:
function-declaration ::= declared-element [: type-expression] [:= expression]
declared-element
::= id f , id g
j id ( parameters )
parameters
::= parameter f , parameter g
parameter
::= id : type-expression j type-expression j id
1.18 Declarac~ao de Func~oes Externas
Uma func~ao externa e uma func~ao denida externamente. Como o seu valor e denido pelo
ambiente externo, elas n~ao possuem um corpo para ser avaliado. Desta forma, a denic~ao de uma
func~ao externa contem somente a especicac~ao do sua assinatura.
A sintaxe para declarac~ao de func~oes externas e dada por:
external-declaration ::= declared-element [: type-expression]
Machna permite que se escreva um programa em outra linguagem, como C, que avalie uma func~ao
externa e retorne o valor para a especicac~ao. Para isso, denimos o protocolo de comunicac~ao de
func~oes externas abaixo:
12
Protocolo de Comunicac~ao de Func~oes Externas
Func~oes externas podem ser func~oes escritas em C, tais que, dados os argumentos, ela retorna o
valor desejado. Desta maneira, e denido um protocolo para a passagem de par^ametros e o valor
de retorno das func~oes, de modo que possamos obter precis~ao na avaliac~ao das func~oes externas.
O protocolo e seguinte:
para cada par^ametro da func~ao externa, existe um par^ametro na func~ao escrita em C;
a ordem dos par^ametros nas duas func~oes deve ser a mesma;
os tipos dos par^ametros e de retorno na func~ao escrita em C devem seguir o tipo do cabecalho
denido para a func~ao externa, seguindo a seguinte equival^encia:
{ Bool, Char e enumerac~oes equivalem ao tipo char de C;
{ Int equivale ao tipo int de C;
{ Real equivale ao tipo double de C;
{ String equivale ao tipo char* de C;
{ um tipo tupla equivale a uma estrutura de C, de modo que os campos da tupla seguem
este protocolo de equival^encias com os campos da estrutura na implementac~ao em C;
{ um tipo lista e recebido e retornado como um arranjo em C, cujo tipo dos elementos
correspondem segundo este protocolo.
Por exemplo, os cabecalhos de func~oes externas abaixo s~ao equivalentes aos cabecalhos de func~oes
em C dados em seguida.
/* Em Mach
na */
type
T is (Int,
external
Bool)
f(x:Int):Int;
g(x,y:Int;c:Char):Bool;
h(a:Int;b:T):T;
:
... x := f(10) ...
... y := g(a,b,c) ...
... z := h(1,d) ...
transition
/* Em C */
typedef
int f(int
struct
x); ...
* equivT;
char g(int x, int y, char c);
equivT h(int a, equivT b);
... x = f(10) ...
... y = g(a,b,c) ...
... z = (1,d) ...
1.19 Denic~ao das Regras de Inicializac~ao
A sec~ao init e utilizada para denic~ao de valores iniciais de func~oes e disparo de agentes. E da
forma
init regra
13
e tem o efeito de executar a regra denida. Esta regra e executada da mesma forma que qualquer
regra, e os valores retornados por func~oes chamadas e o valor que denido na declarac~ao da func~ao
ou o valor default do tipo de retorno da funca~o.
Na sec~ao init, pode-se utilizar tambem a regra create para criar os agentes que ir~ao executar a
regra de transic~ao do modulo.
A sintaxe e dada por:
init-part ::= init transition-rule
1.20 Declarac~ao de Abstrac~oes de Regras
Uma abstrac~ao de regras de transic~ao e semelhante a um procedimento de uma linguagem imperativa como Pascal. Chamaremos este tipo de abstrac~ao de ac~ao. Uma ac~ao pode ser parametrizada.
Abaixo mostramos a sintaxe de uma aca~o:
action-declaration ::= id [(parameters)] := transition-rule end
As regras para deduc~ao dos tipos dos par^ametros de uma transic~ao e id^entica a deduc~ao dos tipos
dos par^ametros de uma func~ao. Qualquer inconsist^encia de tipos causara um erro de compilac~ao.
1.21 Sec~ao de Denic~ao de Regras de Transic~ao
A sec~ao de denic~ao de regras pode aparecer somente em modulos de programas, o que signica
que n~ao pode aparecer em um modulo Machna.
As regras em Machna s~ao as regras denidas no Lipari Guide, acrescidas de outras regras, criadas
com o objetivo de tornar a especicac~ao mais simples e legvel.
Abaixo, mostramos a sintaxe para as regras de transica~o:
transition-rule ::= basic-rule
j forall-rule
j choose-rule
j create-rule
j destroy-rule
j stop-rule
j let-rule
j case-rule
j with-rule
j action-call-rule
1.21.1 Regras Basicas
As regras basicas s~ao as regras de atualizac~ao, bloco e condicional. A sintaxe e dada por:
basic-rule
::= id [(arguments)] := expression
j transition-rule f , transition-rule g
j if expression then transition-rule f elseif-part g [else-part] end
elseif-part ::= elseif expression then transition-rule
else-part ::= else transition-rule
arguments ::= expression f , expression g
14
A regra de atualizac~ao e formada por um identicador, que deve ser um nome de func~ao declarada
como din^amica, uma tupla, que s~ao os argumentos para a determinac~ao do endereco da atualizac~ao, e uma express~ao, cujo valor sera atribudo ao endereco formado pelo identicador e pela
tupla. Na atualizac~ao, uma func~ao din^amica so pode receber func~oes denidas por meio de mapeamento explcito, isto e, sem corpo para ser avaliado. Func~oes estaticas e derivadas n~ao podem
ser atualizadas. Exemplos de atualizac~oes s~ao:
...
x,y : Int;
f,g : Int -> Int;
...
x := y, f(x) := 10, g := f
...
A regra bloco e composta por uma sequ^encia de regras, separadas por vrgula, que devem ser
executadas simultaneamente.
Uma regra condicional tem o efeito de executar a regra, cuja guarda seja a primeira guarda a
avaliar em verdadeiro, na sequ^encia dada. As express~oes que formam as guardas devem ter o tipo
Bool.
1.21.2 Regra forall
Uma regra forall tem a forma
forall e1; e2; :::; ek do regra end
onde os elementos ei s~ao da forma a:A, onde A e um tipo escalar, ou a:sa, onde sa e um conjunto,
ou ainda, da forma a, desde que o tipo de a possa ser deduzido do contexto. O seu efeito e criar
diversas inst^ancias de regra, uma para cada valor possvel de e1 ; e2 ; :::; ek nos domnios dados.
Por exemplo, considere o trecho de codigo abaixo:
type Num = 1..3;
dynamic f(Int,Int):Int;
transition:
forall x:Num,y:Num do
f(x,y) := x + y
end
end
Este codigo e equivalente ao codigo abaixo:
type Num = 1..3;
dynamic f(Int,Int):Int;
transition:
f(1,1)
f(1,2)
f(1,3)
f(2,1)
f(2,2)
f(2,3)
f(3,1)
f(3,2)
f(3,3)
end
:=
:=
:=
:=
:=
:=
:=
:=
:=
2,
3,
4,
3,
4,
5,
4,
5,
6
15
E importante ressaltar que os identicadores denidos em um forall s~ao meta-variaveis, que n~ao
podem, desta maneira, ser lados esquerdos de atualizaco~es.
A sintaxe da regra forall e:
forall-rule
typed-pars-seq
id-seq
set-expression
::=
::=
::=
::=
forall typed-pars-seq do transition-rule end
element-seq f , element-seq g
id j id : type-expression j id : set-expression
expression
1.21.3 Regra choose
A regra choose tem a forma:
choose e1; e2; :::; ek satisfying g do
regra
end
onde e1 ; e2 ; :::; ek s~ao da mesma forma que na regra forall. O seu efeito e escolher aleatoriamente
elementos dos domnios dados que satisfacam a guarda g e executar a regra dada, associando os
nomes de identicadores em e1 ; e2 ; :::; ek aos elementos escolhidos.
choose-rule
::= choose type-pars-seq [satisfying expression] do transition-rule end
typed-pars-seq ::= element-seq f , element-seq g
id-seq
::= id j id : type-expression j id : set-expression
1.21.4 Regras Para Criac~ao e Eliminac~ao de Agentes
Para a criac~ao de um agente, utilizamos a regra create, que tem a forma:
create a1 ; a2; :::; an do
regra
end
onde ai e da forma a:T, ou a, ou T, onde a e um identicador e T e um tipo agente, da forma agent
of M. O efeito desta regra e criar um agente que executara a regra do modulo M. Apos a criac~ao,
este agente e referenciado pela variavel a, e a regra de transic~ao regra e executada, interpretando
esta variavel como o novo agente.
Se o nome do modulo n~ao for explicitado, o compilador tentara inferi-lo pelo contexto; se n~ao for
possvel, ocorrera um erro de compilaca~o.
Para a eliminac~ao de um agente, utilizamos a regra destroy, que tem a forma:
destroy
id
onde id e um nome de func~ao ou variavel, de um tipo agente. O seu efeito e encerrar a execuc~ao
do agente referenciado por id.
Por exemplo, o codigo abaixo cria um agente x que executa a regra associada ao modulo X,
executando as regras de inicializac~ao dadas:
create
do
x:X
numagentes := numagentes + 1,
ready(x) :=
end
true
O codigo abaixo encerra a execuc~ao de todos os agentes que executam a regra do modulo X e
encerra a sua propria execuca~o.
forall x : agent of X do
destroy x
end,
destroy self
16
E interessante notar que destroy self e equivalente a regra stop.
A sintaxe para as regras create e destroy e dada por:
create-rule
destroy-rule
typed-pars-seq
id-seq
::=
::=
::=
::=
create typed-pars-seq do transition-rule end
destroy id
element-seq f , element-seq g
id j id : type-expression
1.21.5 Regra Para Parada
De acordo como o modelo ASM, a regra de transic~ao de um agente e executada repetidamente. A
regra para parada da maquina e a regra stop. Quando executada, esta regra faz com que a regra
do modulo do agente n~ao seja executada novamente, para que o agente encerre sua execuca~o. Isto
signica que, quando o stop for executado, o passo em que ele for executado e terminado, para,
a partir deste momento, a execuc~ao da maquina realmente terminar.
Por exemplo, no estado nal da execuc~ao abaixo, o valor de a e 20:
module C
dynamic a := 0;
transition:
if a < 10 then
a := a + 10
else
a := a + 10,
stop
end
end
A sintaxe da regra stop e:
stop-rule ::= stop
1.21.6 Regra let
Uma regra let e utilizada para fazer declarac~oes que sejam locais a uma regra. Tem a seguinte
sintaxe:
let-rule
::= let declaration-in-let f ; declaration-in-let g in transition-rule end
declaration-in-let ::= id = expression
Por exemplo, o trecho de codigo
...
let
a
b
c
x
=
=
=
=
head(L);
head(tail(L));
head(tail(tail(L)));
a + b + c
in
g(10)
end
:= x * (a + 1) * (b + c)
...
17
declara os identicadores a, b, c e x, cujo escopo e a regra
g(10) := x * (a + 1) * (b + c)
E importante ressaltar que os identicadores denidos em uma regra let s~ao meta-variaveis que
representam right values, n~ao podendo ser, desta maneira, alvos de atribuic~oes.
1.21.7 Regra case
Uma regra case e uma regra condicional, na qual todas as guardas s~ao da forma
expression = valor manifesto
A sintaxe para esta regra e dada por:
case-rule
::= case expression of f case-rule-atom g [case-rule-otherwise] end
case-rule-atom
::= expression -> transition-rule
case-rule-otherwise ::= otherwise -> transition-rule
Por exemplo, a regra abaixo e equivalente a regra mostrada acima:
case
head(s) * head(tail(s))
1 -> ...
4 -> ...
9 -> ...
16 -> ...
25 -> ...
-> ...
of
otherwise
end
1.21.8 Regra with
Uma regra with e uma forma de case, na qual, ao inves de compararmos o valor de uma express~ao
com express~oes manifestas, comparamos o seu tipo com nomes de tipo.
A sintaxe para esta regra e a seguinte:
with-rule
::= with expression as f with-rule-atom g [with-rule-otherwise] end
with-rule-atom
::= [id :] type-expression -> transition-rule
with-rule-otherwise ::= otherwise -> transition-rule
Por exemplo, a regra abaixo utiliza o tipo do primeiro elemento de uma lista para determinar a
ac~ao a ser tomada:
list : List;
...
head(list)
i:Int -> transition rules for integer head
b:Bool -> transition rules for boolean head
s:String -> transition rules for string head
-> transition rules for other cases
with
as
otherwise
end
18
1.21.9 Regra de Chamada a Ac~oes
Uma regra de chamada a ac~ao e equivalente a uma chamada de procedimentos em uma linguagem
imperativa, com a excec~ao de que a sua execuca~o gera um conjunto de atualizac~oes que e tratado
como o conjunto de atualizac~oes de uma regra comum. Os par^ametros de uma ac~ao, que forem
atualizados, ser~ao tratados como sin^onimos para os argumentos no ponto de chamada. Demais
argumentos s~ao avaliados e substitudos pelos par^ametros formais da declarac~ao da ac~ao.
A utilizac~ao de ac~oes permite escrevermos denic~oes menores e mais legveis, utilizando abstrac~oes
de regras.
A sintaxe de chamadas a aco~es e:
action-call-rule ::= id [(arguments)]
arguments
::= expression f , expression g
Por exemplo, a regra abaixo e uma chamada a uma transic~ao:
...
action
...
end
t(x:Int) // declara a a
c~
ao t
...
// Rules...
t(1), t(2), t(3) // chama a a
c~
ao t...
...
1.22 Invariante da Execuc~ao
Em um modulo, pode-se denir uma condic~ao que deve ser satisfeita toda vez que a sua regra de
transic~ao for executada. Chamamos esta condic~ao de invariante. Para denirmos o invariante da
regra de transic~ao, denimos uma sec~ao invariant, que contem a express~ao booleana do invariante.
A sua forma e
invariant: express~ao-booleana
O invariante deve ser testado antes e depois de cada passo. Se em algum momento ele n~ao for
satisfeito, ocorre um erro de execuc~ao.
Em um modulo Machna, pode haver tambem uma sec~ao de invariante, semelhante a um modulo
qualquer. Entretanto, os elementos que podem aparecer na express~ao do invariante s~ao somente
os literais booleanos, true e false, os operadores logicos, and, or, not e xor, e invariantes de
modulos, referenciados como M.invariant, onde M e um nome de modulo. Este invariante vale
para a execuc~ao de todo os modulos criados a partir do modulo Machna, sendo igualmente testado
antes e depois da execuc~ao de cada passo, independente de qual agente sera executado.
1.23 Sintaxe de Express~oes
As express~oes de Machna s~ao as seguintes: express~oes sobre os tipos basicos, listas, conjuntos,
tuplas, mapeamentos, convers~ao de tipos, condicionais, let e outras express~oes.
1.23.1 Operadores de Machna
Os operadores de Machna s~ao mostrados na tabela abaixo. A ordem de apresentac~ao mostra a
preced^encia dos operadores, sendo que os de preced^encia mais alta est~ao na primeira linha e os de
preced^encia mais baixa est~ao no m.
19
- (un
ario)
* / %
+ = != < > <= >=
preced^encia mais alta
and
or xor
in
::
->
preced^encia mais baixa
1.23.2 Valores Booleanos
As express~oes com o tipo Bool s~ao:
os literais true e false;
qualquer aplicac~ao de func~ao (ver Sec~ao 1.23.7), ou operac~ao binaria, como por exemplo, a
aplicac~ao dos operadores relacionais, cujo tipo de retorno seja equivalente ao tipo Bool;
a operac~ao unaria de negac~ao logica, utilizando o operador pre-xado not;
as operac~oes binarias que utilizam os operadores logicos and (conjunc~ao), or (disjunc~ao) e
xor (or exclusivo).
Exemplos de express~oes booleanas s~ao:
e.
f(x) = 21, y * a > 5
and
cond, b
and c xor d or
1.23.3 Caracteres
As express~oes com o tipo Char s~ao:
os literais caracteres, que representam os caracteres da tabela ASCII;
qualquer aplicac~ao de func~ao (ver Sec~ao 1.23.7), cujo tipo de retorno seja equivalente ao tipo
Char;
as func~oes pre-denidas sobre o tipo Char, dadas abaixo:
ord(Char):Int
chr(Int):Char
{ Retorna o codigo ASCII do caractere;
{ Retorna o caractere com o codigo ASCII dado.
Exemplos de express~oes com o tipo Char s~ao:
`a', `1', '\n', chr(13), ord(`\n').
1.23.4 Numeros Inteiros
As express~oes com o tipo Int s~ao:
os literais inteiros, que representam os numeros inteiros, com valor mnimo -2147483648 e
maximo 2147483647. Estes literais podem ser representados na forma decimal (sequ^encia
de um ou mais dgitos de 0 a 9), octal (sequ^encia de 1 ou mais dgitos de 0 a 7, precedida
sempre por um 0) ou hexadecimal (sequ^encia de 1 ou mais dgitos de 0 a 9 ou letras de A a
Z, precedida sempre por 0x);
a operac~ao unaria de negac~ao, utilizando o operador -;
as operac~oes binarias de adic~ao (+), subtrac~ao (-), multiplicac~ao (*), divis~ao (/) e resto da
divis~ao (%);
20
qualquer aplicac~ao de func~ao (ver Seca~o 1.23.7), cujo tipo de retorno seja equivalente ao tipo
Int;
as func~oes pre-denidas sobre o tipo Int, dadas abaixo:
{ valor absoluto de um numero inteiro;
max(Int,Int):Int { m
aximo entre dois inteiros;
min(Int,Int):Int { mnimo entre dois inteiros;
sqr(Int):Int { quadrado de um n
umero inteiro.
abs(Int):Int
Exemplos de express~ao com numeros inteiros s~ao:
max(a,b) - sqr(min(x,y) + 1).
x + 1, x * 2 + y * 5 - 10 % v, abs(x) +
1.23.5 Numeros Reais
As express~oes com o tipo Real s~ao:
os literais reais, que representam numeros de ponto utuante do padr~ao IEEE 754, com 1.79769313486231570E+308 como valor maximo e 4.94065645841246544E-324 como valor
mnimo;
a operac~ao unaria de negac~ao, utilizando o operador -;
as operac~oes binarias de adic~ao (+), subtraca~o (-), multiplicac~ao (*) e divis~ao (/);
qualquer aplicac~ao de func~ao (ver Seca~o 1.23.7), cujo tipo de retorno seja equivalente ao tipo
Real;
as func~oes pre-denidas sobre o tipo Real, dadas abaixo:
abs(Real):Real { valor absoluto de um n
umero real;
max(Real,Real):Real { m
aximo entre dois numeros reais;
min(Real,Real):Real { mnimo entre dois n
umeros reais;
sqr(Real):Real { quadrado de um n
umero real;
sqrt(Real):Real { raiz quadrada de um n
umero real.
1.23.6 Cadeias de Caracteres
As express~oes sobre o tipo String s~ao:
os literais cadeias de caracteres, que s~ao sequ^encias de zero ou mais caracteres, envolvidas por
aspas; o padr~ao de cadeias de caracteres de Machna e de cadeias de caracteres terminadas
com nulo;
a operac~ao binaria de concatenac~ao, utilizando o operador +;
qualquer aplicac~ao de func~ao (ver Sec~ao 1.23.7), cujo tipo de retorno seja equivalente ao tipo
String;
a func~ao pre-denida length(String):Int, que retorna o comprimento da cadeia de caracteres.
Exemplos de express~oes com cadeias de caracteres s~ao:
21
"string\n", length(``abcd"+ nome).
1.23.7 Aplicac~ao de Func~oes
A aplicac~ao de func~ao tem a forma geral
nome de func~ao(argumentos)
onde argumentos e uma lista de express~oes, cujo comprimento e igual a aridade da func~ao da
aplicac~ao. Se a aridade da func~ao for igual a zero, ent~ao n~ao se utilizam os par^enteses, somente
o nome da func~ao. Os tipos dos argumentos devem ser equivalentes aos tipos esperados como
par^ametros.
Exemplos de aplicac~oes de func~ao: x, f(1,2,true), f(x,g(y+1,h)), chr(0).
1.23.8 Listas
Machna possui dois tipos de listas: listas genericas e listas de elementos de um tipo especco.
Uma lista vazia e dada pelo literal nil. Sobre listas, est~ao denidas as seguintes operac~oes:
x::list
concat(list1, list2)
head(list)
tail(list)
lenght(list)
retorna uma lista cuja cabeca e x e cuja cauda e list
retorna a concatenac~ao das listas list1 e list2
retorna o elemento na cabeca de list
retorna a cauda de list
retorna o comprimento de list
Em tempo de compilac~ao, s~ao feitos testes para consist^encia e infer^encia de tipos. As regras para
consist^encia de tipos s~ao as seguintes:
1. na operac~ao x::list, se x possuir o tipo X, ent~ao list deve ser do tipo list of X ou List;
2. na operac~ao cat(list1, list2), list1 e list2 devem ser listas do mesmo tipo, a menos
que uma delas seja do tipo List; se o tipo de uma delas for List, ent~ao o resultado e do
tipo List;
3. se list for do tipo list of X, ent~ao head(list) e do tipo X; se list for do tipo List, ent~ao
head(list) ser
a do tipo \?";
4. a express~ao tail(list) tem o mesmo tipo de list.
Um agregado lista e da forma
[t1 ; t2 ; :::; tn ]:
Se todos as express~oes forem do mesmo tipo X, ent~ao o tipo da express~ao toda e list of X; caso
contrario, o tipo sera List.
1.23.9 Conjuntos
Assim como listas, conjuntos podem ser genericos ou de um tipo especco. As operac~oes envolvendo conjuntos s~ao:
s1 + s2
s1 - s2
s1 * s2
x
s
s(x)
s1 relop s2
card(s)
in
uni~ao
diferenca
intersec~ao
pertin^encia
pertin^encia
inclus~ao (<=), igualdade (=), etc.
cardinalidade do conjunto
22
Um agregado conjunto e da forma
ft1 ; t2 ; :::; tn g:
Se todos as express~oes forem do mesmo tipo X, ent~ao o tipo da express~ao toda e set of X; caso
contrario, o tipo sera Set.
Conjuntos podem ser utilizados em regras da seguinte maneira:
Regra de atualizac~ao:
e
s(t) :=
true s
:= s +
f
s(t) :=
false s
:= s -
ftg
t
g
Regra forall: se s e do tipo set of X, ent~ao a construc~ao
forall x:s do regra end
instancia regra substituindo x com cada valor pertencente a s, executando todas as inst^ancias em paralelo;
Regra choose: se s e do tipo set of X, ent~ao a construc~ao
choose
x:s
do
regra
end
escolhe aleatoriamente um elemento e pertencente ao conjunto s e executa regra, associando
x a e.
1.23.10 Tuplas
Uma tupla de Machna e uma sequ^encia de tamanho xo, cujos elementos podem ser de quaisquer
tipos.
Uma express~ao da forma T(t1, t2, t3) cria uma tupla do tipo T, formada pelos elementos t1,
t2 e t3. O acesso aos elementos de uma tupla e feito sempre pelo seus rotulos, como no exemplo
abaixo:
...
type
is
Pair
(x,y:Int);
p1, p2 : Pair;
...
p1 := Pair(1,2),
p2.x := p1.y
...
1.23.11 Mapeamentos
Um mapeamento e um conjunto de associac~oes de valores de um domnio a valores de um contradomnio. Por exemplo, considere o fragmento de codigo abaixo:
static
f
f :=
f1
g
-> 2, 2 -> 3, 3 -> 4
e uma func~ao de inteiros para inteiros, tal que:
f(1) = 2, f(2) = 3, f(3) = 4
O valor da aplicac~ao de f a algum outro valor, que n~ao especicado no conjunto, e o valor default
do contradomnio.
23
O operador -> cria um par que pode ser inserido em algum conjunto. Um mapeamento e semelhante a um conjunto de pares, isto e, uma relaca~o, com a diferenca que, se x e um conjunto de
pares e y e um mapeamento, ent~ao e possvel que, para quaisquer a, b e c, (a; b) 2 x e (a; c) 2 x.
Entretanto, (a; b) 2 y e (a; c) 2 y so e possvel se b = c.
As operac~oes que podem ser realizadas sobre mapeamentos s~ao a aplicac~ao de func~ao, da forma
f (a1 ; :::; an ), a atualizac~ao de func~oes din^amicas, da forma f (a1 ; :::; an ) := b e a comparac~ao por
= (igualdade) e != (diferen
ca).
1.23.12 Convers~ao de Tipos
As express~oes abaixo realizam a convers~ao de tipos, para os casos em que e necessario, como por
exemplo, utilizac~ao de valores do tipo ?. Os dois tipos de express~oes que t^em essa nalidade s~ao
as express~oes with e is e a convers~ao explcita de tipos.
A express~ao with tem a forma:
with e as
e1 : T1
e2 : T2
->
->
b1
b2
en : Tn
->
bn
...
otherwise
end
->
bn+1
Se as express~oes b1 ; b2 ; :::; bn ; bn+1 tiverem o mesmo tipo X, ent~ao o tipo da express~ao e X. Caso
contrario e ?. A clausula otherwise e obrigatoria, a menos que as clausulas de coerc~ao sejam
exaustivas. Assim, se o tipo de e for ?, esta clausula e obrigatoria. O valor desta express~ao e
obtido, comparando-se o tipo de e com os tipos das clausulas as. Se a i-esima clausula casar com
o tipo de e, ent~ao, associamos ei ao valor de e e retornamos o valor de bi . Se nenhuma clausula
casar com o tipo de e, ent~ao o valor retornado e o valor de bn+1 .
Por exemplo, considere o fragmento de codigo:
...
dynamic x : List; // Os elementos de
...
with head(x) as
a:Int -> 1 + a
b:Bool -> if b then 1 else 0 end
c:Real -> round(c)
otherwise -> 4
end
x podem ser de qualquer tipo
...
No exemplo abaixo, a clausula otherwise n~ao e necessaria, pois as clausulas as s~ao exaustivas.
...
type X is Bool | Int
dynamic x : X;
...
with x as
| Real;
a:Int -> 1
b:Bool -> 2
c:Real -> 3
end
24
...
O operador binario is e um operador de inspec~ao de tipos, que recebe como argumentos uma
express~ao e um nome de tipo e retorna verdadeiro se o tipo da express~ao for igual ao tipo dado.
Um exemplo da utilizac~ao do operador is esta no codigo abaixo:
...
type X is Bool | Int
dynamic x : X;
...
if x is Int then
...
elseif x is Bool then
...
else
...
end
| Real;
...
O casting explcito de tipos e uma express~ao da forma (T )e. O seu efeito e fazer a convers~ao
explcita de e para um valor do tipo T . Se a convers~ao n~ao puder ser feita, ocorrera um erro de
execuca~o.
1.23.13 Condicionais e Let
Nesta categoria se enquadram as expresss~oes condicionais if e case e a express~ao let. A estrutura
destas express~oes e equivalente as regras de transic~ao de mesmos nomes, com algumas diferencas:
a parte else da express~ao if e obrigatoria;
a clausula otherwise da express~ao case e obrigatoria, a menos que as clausulas sejam
exaustivas, como por exemplo, se cobrirem todos os elementos de uma enumerac~ao;
se os tipos das express~oes resultantes de cada parte do if e do case s~ao o mesmo tipo X ,
ent~ao o tipo da express~ao toda e X ; caso contrario e ?.
1.23.14 Express~oes Especiais
A express~ao default retorna o valor default do tipo esperado. Para cada tipo existe um valor
default pre-denido. A express~ao self retorna a identicac~ao ao agente que estiver executando a
regra.
Exemplos:
algebra:
static
default
default
default
default
fg
list of
default
default
transition
a
b
c
d
e
f
:
:
:
:
:
:=
Int :=
// x := 0
Bool :=
// x := false
Real :=
// x := 0.0
Set :=
// x :=
Int :=
// x := nil
// f := undef, pois undef e o default de ?
:
...
hungry(self) := true, // Atualiza as fun
c~
oes locais ao agente
25
thinking(self) := false
...
1.23.15 Gramatica das Express~oes
A sintaxe das express~oes e:
expression
::= literal
j unop expression
j expression binop expression
j mod-function-call
j agregate
j if-expression
j case-expression
j let-expression
j with-expression
j expression . expression
j [module-name .] id [(arguments)]
j
j
j
literal
::=
unop
binop
::=
::=
agregate
::=
if-expression
if-expr-elseif
if-expr-else
let-expression
case-expression
case-expr-atom
case-expr-default
with-expression
with-expr-atom
with-expr-default
::=
::=
::=
::=
::=
::=
::=
::=
::=
::=
j
j
j
j
self
default
(expression)
false j true j char-literal j integer-literal
oat-literal j string-literal j nil
; j not j (type-name)
j = j % j + j ; j = j ! = j < j > j <= j >=
and j or j xor j :: j in j is
\["expression f , expression g\]"
\f"expression f , expression g \g"
type-name ( expression f , expression g )
if expression then expression f if-expr-elseif g if-expr-else end
elseif expression then expression
else expression
let declaration-in-let f ; declaration-in-let g in expression end
case expression of f case-expr-atom g [case-expr-default] end
expression ! expression
otherwise ! expression
with term f with-expr-atom g [with-expr-default] end
[id :] type-name ! expression
otherwise ! expression
1.24 Manipulac~ao de Arquivos
Para manipulac~ao de arquivos, existem os tipos pre-denidos InputStream, OutputStream e o
construtor de tipos le of, que recebe como argumento um tipo.
O tipo pre-denido InputStream representa um arquivo texto para leitura com caracteres de
leiaute. As operac~oes (ac~oes) que podem ser feitas sobre este tipo s~ao:
{ ac~ao pre-denida que abre, para leitura, o arquivo de
para este arquivo no par^ametro input;
close(InputStream input) { a
c~ao pre-denida, que fecha o arquivo referenciado por input;
readInt(InputStream input, Int i) { l^
e um valor inteiro do arquivo input e coloca o resultado
em i;
open(InputStream input, String s)
nome s, colocando uma refer^encia
26
readChar(InputStream input, Char c)
em c;
readReal(InputStream input, Real r)
coloca o resultado em r;
{ l^e um caractere do arquivo input e coloca o resultado
{ l^e um numero ponto-utuante do arquivo
readString(InputStream input, String s)
coloca o resultado em s.
input
e
{ l^e uma cadeia de caracteres do arquivo input e
O tipo pre-denido OutputStream e analogo ao tipo OutputStream, e representa um arquivo texto,
para escrita, com caracteres de leiaute. As operac~oes (ac~oes) que podem ser feitas sobre este tipo
s~ao:
open(OutputStream output, String s) { a
c~ao pre-denida que abre, para escrita,
de nome s, colocando uma refer^encia para este arquivo no par^ametro output;
o arquivo
{ aca~o pre-denida, que fecha o arquivo referenciado por output;
writeInt(OutputStream output, Int i) { escreve o valor de i no arquivo output;
writeChar(OutputStream output, Char c) { escreve o valor de c no arquivo output;
writeReal(OutputStream output, Real r) { escreve o valor de r no arquivo output;
writeString(OutputStream output, String s) { escreve o valor de s no arquivo output;
close(OutputStream output)
Uma express~ao de tipo leofT , onde T e um tipo, cria um tipo que representa arquivos, cujos
elementos s~ao do tipo T . Estes arquivos s~ao binarios, com acesso sequencial ou direto. As operac~oes
(ac~oes) que podem ser feitas s~ao:
le of T tFile, String s, Bool readOnly) { ac~ao pre-denida que abre, para leitura ou para escrita, o arquivo de nome s, colocando uma refer^encia para este arquivo no
par^ametro tFile; o arquivo sera de leitura de o par^ametro readOnly for verdadeiro, caso
contrario, sera de escrita;
close(le of T tFile) { a
ca~o pre-denida, que fecha o arquivo referenciado por tFile;
read(le of T tFile, T t) { l^
e um valor do tipo T, do arquivo referenciado por tFile, e coloca
este valor em t;
write(le of T tFile, T t) { escreve o valor de tipo t, no arquivo referenciado por tFile;
open(
Sobre todos os arquivos s~ao denidas as func~oes eof e status. A func~ao eof(f:File):Bool
recebe como argumento um arquivo de qualquer tipo e retorna true, se o arquivo estiver no m,
ou false, caso contrario. A func~ao status(f:File):Int retorna o status do arquivo como um
numero inteiro, de acordo com a tabela abaixo:
0
1
2
3
arquivo fechado
arquivo aberto
erro de leitura no arquivo
erro de escrita no arquivo
A menos da funca~o status, qualquer operac~ao sobre um arquivo fechado gera um erro de execuc~ao.
E importante salientar que, por causa do modelo algebrico, qualquer operac~ao de leitura em
arquivos so e percebida no proximo estado. Da mesma forma, qualquer chamada a status em um
mesmo estado retorna o mesmo valor, que e o status do arquivo no passo anterior. Assim como
qualquer ac~ao de Machna, a ordem de execuc~ao de duas operac~oes sobre arquivos, no mesmo,
estado n~ao e garantida. Por exemplo, considere o codigo abaixo:
27
...
f : InputStream;
g : OutputStream;
...
transition:
readInt(f,a),
readInt(f,a),
readInt(f,b),
writeInt(g,x),
writeInt(g,y),
end
Ser~ao lidos tr^es valores do arquivo f e escrito dois valores no arquivo g. Entretanto, n~ao ha como
determinar qual sera o valor de a e qual sera o valor de b, pois isto dependera da ordem em que o
compilador escolher executar este codigo. Da mesma forma, n~ao e possvel determinar qual valor
sera escrito antes em g, se o valor de x ou se o valor de y.
28
Cap
tulo 2
Exemplos
2.1 Pesquisa Binaria
Os modulos abaixo especicam um agente que realiza a pesquisa binaria.
module PesqBin
algebra:
static n : Int := 100;
type
Index is 1..n;
Array is Index -> Int;
external
key : Int;
array;
dynamic
k, pos, inf, sup : Int;
encontrado : Bool;
array1;
init
array1 := array
k := key, pos := (n+1)/2, inf := 1, sup := n
encontrado :=
:
mean = (inf+sup)/2
false
transition
let
in
if not encontrado and inf < sup then
if array1(mean) = k then encontrado := true,
elseif array1(mean) < k then inf := mean + 1
else sup := mean - 1
end
end
end
end
machina PesquisaBinaria
create PesqBin
end
29
pos := mean
2.2 Ordenac~ao por Selec~ao
O modulo abaixo especica a ordenac~ao por seleca~o.
module Selecao
algebra:
static n : Int := 100;
type
Index
Array
is 1..n;
is Index ->
external
Int;
n : Int;
array;
dynamic
modo, i, k, j :
array1;
Int;
init
array1 := array,
modo := 1, i := 1, k := 1, j := 1
:
modo = 1
i < n
k := i, j := i + 1, modo := 2
modo = 2
j := j + 1,
j > n
modo := 3
f(j) < f(k)
k := j
transition
if
and
then
elseif
then
if
then
elseif
then
end
else modo = 3 then
i := i + 1, modo := 1,
if k != i then
f(k) := f(i), f(i) := f(k)
end
end
end
machina OrdenacaoPorSelecao
create ops : Selecao
end
2.3 Numeros Primos
O programa abaixo especica um algoritmo para busca de numeros primos.
machina MarcaPrimos
algebra:
type
Num is 2..1000;
dynamic
primo : Num -> Bool;
init
forall n:Num do primo(n)
transition:
:=
true end
30
forall num1,num2 do
if num2 < num1 and num1%num2 = 0 then
primo(num1) := false
end
end
end
O programa abaixo e equivalente ao anterior, mas utiliza outros recursos de Machna:
machina
algebra:
type
MarcaPrimos
is
is set of
default f2..1000g;
dynamic
primo : Numset;
transition:
forall num1,num2 do
if num2 < num1 and num1%num2 = 0 then
primo(num1) := false
end
end
end
Num
2..1000;
Numset
Num
machina DeterminaPrimos
create mp : MarcaPrimos
end
2.4 Especicac~ao da Sem^antica de Tiny
Tiny e uma linguagem imperativa de pequeno porte que contem somente comandos e express~oes.
A denic~ao de Tiny sera feita em cinco modulos:
1. Modulo principal (Tiny) { contem a regra principal da especicac~ao e as rotinas de inicializac~ao;
2. Modulo de Express~oes (Expressions) { contem as regras de avaliac~ao de express~oes;
3. Modulo de Comandos (Commands) { contem as regras de execuc~ao de comandos;
4. Modulo de Operac~oes (Operations) { contem as regras de operac~ao na pilha.
5. Modulo de Globais (Globals) { contem as declarac~oes dos principais tipos e func~oes da
especicac~ao de Tiny.
2.4.1 Modulo de Globais (Globals)
module Globals
algebra:
type
public Undefined is public enum fundefinedg;
public Id is String;
public Program is List;
public Input is list of Int;
31
public Output is list of Int;
public Value is Bool | Int;
public Memory is Id ! (Value | Undefined) default undefined;
public KeyWord is
ftadd, tassign, tcond, texchange, tequals tnot, toutput, tread,
public Opstack is List;
external
p:Program;
i:Input;
dynamic
public program := p, input
public memory;
public error := false
end
:= i, output := nil, opstack := nil;
2.4.2 Modulo de Operaco~es (Operations)
module Operations
import:
Globals(program,output,input,opstack,error,memory);
algebra:
action
treatOutput :=
if head(program) is x:Int then
output := concat(output, [x]),
program := tail(program),
opstack := tail(opstack)
else
error
end
end;
:=
true
treatAssign
opstack := tail(tail(opstack)),
memory((String)head(tail(opstack))) := (Globals.Value)head(program)
;
treatExchange :=
opstack := tail(opstack),
program := head(tail(program))::head(program)::tail(tail(program))
;
treatAdd :=
end
end
let
in
hp = head(program);
htp = head(tail(program));
if
is
and
is
then
hp
Int
htp
Int
program := ((Int)x + (Int)y)::tail(tail(program)),
opstack := tail(opstack)
else
error
end
end
end;
:=
true
treatNot :=
32
g
twhile ;
if
is
not
then
head(program)
Bool
program := (
((Bool)b))::tail(program),
opstack := tail(opstack)
else
error := true
end
end;
treatCond :=
if head(program) is Bool then
if (Bool) head(program) then
program := head(tail(program))::tail(tail(tail(program)))
else
program := tail(tail(program))
end,
opstack := tail(opstack)
else
error := true
end
end;
treatEquals :=
let
in
hp = head(program);
htp = head(tail(program));
if
is
and
is
then
hp
Int
htp
Int
program := ((Int)x = (Int)y)::tail(tail(program)),
opstack := tail(opstack)
else
error := true
end
end
end;
public treatValue :=
if head(opstack) is Globals.KeyWord then
case (Globals.KeyWord) head(opstack) of
Globals.toutput -> treatOutput;
Globals.tassign -> treatAssign;
Globals.texchange -> treatExchange;
Globals.tadd -> treatAdd;
Globals.tnot -> treatNot;
Globals.tcond -> treatCond;
Globals.equals -> treatEquals
end
end
else
error
end
end
:=
true
2.4.3 Modulo de Express~oes (Expressions)
module Expressions
import:
33
Globals(program,output,input,opstack,error,memory);
algebra:
action
public readMemory :=
let
id = (String) head(program)
in
if memory(id) = undef then
error := true
else
program := memory(s) :: tail(program)
end
end
end;
public treatNot :=
program := tail(program),
opstack := Globals.tnot::opstack
;
treatEquals :=
program := tail(program),
opstack := Globals.tequals::opstack
;
treatAdd :=
program := tail(program),
opstack := Globals.texchange::Globals.tadd::opstack
;
treatRead :=
input = nil
error := true
end
public
end
public
end
public
if
else
then
program := head(input)::tail(program),
input := tail(input)
end
end
end
2.4.4 Modulo de Comandos (Comandos)
module Commands
import:
Globals(program,output,input,opstack,error,memory);
algebra:
action
public treatAssign :=
program := tail(tail(program)),
opstack := Globals.tassign::head(tail(program))::opstack
;
treatOutput :=
program := tail(program),
opstack := Globals.toutput::opstack
;
treatConditional :=
program := tail(program),
end
public
end
public
34
opstack := Globals.tcond::opstack
end;
public
let
in
treatWhile :=
second = head(tail(program));
third = head(tail(tail(program)));
whileExp = second;
whileCom = Globals.twhile::second::third::nil;
whileTrue = third::whileCom::nil;
whileCont = tail(tail(tail(program)));
program := whileExp::whileTrue::nil::whileCont,
opstack := Globals.tcond::opstack
end
end
end
2.4.5 Modulo principal (Tiny)
module Tiny
import:
Commands, Expressions, Operations,
Globals(program,output,input,opstack,error,memory);
:
flatProgram :=
program := concat((List) head(program), tail(program))
algebra
action
end
transition:
if program != nil and not
with head(program) as
error
then
l:List -> flatProgram;
s:String -> Expressions.readMemory;
p:Globals.KeyWord ->
p
Globals.tnot -> Expressions.treatNot;
Globals.tequals -> Expressions.treatEquals;
Globals.tadd -> Expressions.treatAdd;
Globals.tread -> Expressions.treatRead;
Globals.tassign -> Commands.treatAssign;
Globals.toutput -> Commands.treatOutput;
Globals.tcond -> Commands.treatConditional;
Globals.twhile -> Commands.treatWhile;
;
x:Globals.Value -> Operations.treatValue
case of
end
end
end
end
2.4.6 Disparo do Agente de Execuc~ao
machina TinySemantics
create tny : Tiny
end
35
2.5 Jantar dos Filosofos
Este e um exemplo de especicac~ao com varios agentes, onde todos executam o mesmo programa,
de maneira concorrente. Para explicitar a concorr^encia, deniremos a regra de transic~ao como
intercalada (interleaved).
module DinPh
algebra:
static n : Int := 5;
type PhId is 1..n;
dynamic
initialized, thinking, hungry, eating :
leftFork, rightFork : PhId -> Bool;
myId : DinPh -> PhId;
:
inicializado(self)
thinking(self) :=
,
initialized(self) :=
DinPh -> Bool;
transition
if not
then
true
true
else
if thinking(self) then
thinking(self) := false, hungry(self) := true
elseif hungry(self) then
if not leftFork(myId(self)) and not rightFork(myId(self)) then
eating(self) := true, hungry(self) := false,
leftFork(myId(self)) := true,
rightFork(myId(self)) := true
end
else
eating(self) := false, hungry(self) := true
end
end
end
O modulo Machna que dispara os agentes e dado abaixo:
machina DiningPhilosophers
create5 DinPh
end
36