Métodos Formais em Engenharia de Software 4

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Conteudista: Prof. Me. Artur Marques  
Revisão Textual: Prof.ª Dra. Selma Aparecida Cesarin 
 
Objetivo da Unidade:
Conhecer as Notações mais utilizadas em Métodos Formais.
˨ Material Teórico
˨ Material Complementar
˨ Referências
Notações Formais
Notação Formal B 
O Método B é um Método Formal de Desenvolvimento de Software de amplo espectro que
cobre o Processo de Software desde a especi�cação até a implementação. Ele utiliza Máquinas
de Estado, de�nidas em Lógica e Teoria dos Conjuntos, que exportam operações.
Foi originalmente desenvolvida na década de 80 do século XX por Jean-Raymond Abrial.
B tem sido usada nas principais aplicações de Sistema de Segurança Crítica na Europa e tem
suporte de ferramenta robusto e disponível comercialmente para especi�cação, design, prova e
geração de código.
Mas a história de B não é tão simples e nem tão linear quanto simpli�camos no parágrafo
anterior.
Ela é um descendente da Linguagem de programação BCPL, que pouca gente conhece, mas B
foi projetado e implementado pela primeira vez por Dennis MacAlistair Ritchie, um dos
criadores da Linguagem C, junto com Brian Wilson Kernighan, ambos do time de Kenneth
Lane Thompson da Bell Telephone Laboratories, três gênios a quem, sem dúvida alguma,
grande parte do Mundo Digital que existe hoje deve sua existência. Ritchie e Thompson
criaram também o Sistema Operacional Unix.
Você deve ter percebido que a Linguagem B veio antes da Linguagem C. Por isso, a sequência
de letras e, de quebra, agora você sabe porque C se chama C.
1 / 3
˨ Material Teórico
Kenneth Lane Thompson 
Clique no botão para conferir o conteúdo.
ACESSE
Dennis MacAlistair Ritchie 
Clique no botão para conferir o conteúdo.
ACESSE
Brian Wilson Kernighan 
Clique no botão para conferir o conteúdo.
ACESSE
B é especialmente adequado para aplicativos que envolvem cálculos não numéricos. Esses
Programas podem envolver decisões lógicas, operações em inteiros e cadeias de caracteres e
manipulação de bits de baixo nível.
Todos os Programas B são compostos por uma ou mais "funções". Essas funções são como
as funções e subrotinas de um Programa Fortran ou os procedimentos de PL/I.
Leitura 
Saiba mais sobre esses três gigantes acessando os links abaixo. 
https://computerhistory.org/profile/ken-thompson/
https://computerhistory.org/profile/dennis-ritchie/
https://en.wikipedia.org/wiki/Brian_Kernighan
Qualquer função pode invocar qualquer outra função. Ele também pode chamar a si mesmo
recursivamente. Quando uma função é chamada, o chamador pode passar zero ou mais
argumentos para a função chamada. Portanto, o processo de chamar funções em B é muito
parecido com os processos correspondentes em outras Linguagens de Programação.
Cada programa B funcional tem uma função chamada MAIN. O mais importante sobre as
variáveis em B é que elas não têm tipo.
A partir do exemplo a seguir, se você já viu minimamente C, perceberá que B guarda espantosa
semelhança.
Veja:
Uma função pode ter quantas [auto] instruções forem necessárias ou desejadas, mas todas
devem vir antes de qualquer uma das instruções executáveis da função.
A nossa func(z) serve para retornar o valor da operação feita a cada linha de instrução do
Código exemplo acima e retornar o total em [z], nesse caso [z]=21.
As variáveis automáticas, no nosso caso [z], de uma função passam a existir quando a função
é chamada e desaparecem quando a função retorna.
func (z) { 
 auto b, a, k; 
 a = 3; 
 k = 7; 
 b = (z + k) * a; 
 return (b); 
} 
Então, elas não podem ser inicializadas no início da execução, porque elas realmente não
existem no início da execução. Portanto, só receberão valores quando a função é chamada.
Entretanto, todas as outras variáveis, em nosso caso [b,a,k] na função contêm “lixo daquela
posição de memória ou algum caractere espúrio” quando a função é invocada e, portanto,
devem ter valores atribuídos explicitamente antes de serem usadas, em nosso caso [a=3; k=7;
b = (z + k) * a].
Vamos ver um outro exemplo que explora variáveis externas.
Primeiramente, você já percebeu que as variáveis externas são especi�cadas fora do corpo da
função [randnm]. Essa é uma das razões para o nome [extern], porque variáveis externas
devem ser especi�cadas fora do corpo de qualquer função em Notação B.
Em segundo, as variáveis externas são seguidas por números entre colchetes, quando são
especi�cadas fora do corpo da função. É como inicializamos as variáveis nesse caso
[ultimonum=1 e embaralhar=1594323] e embaralhar tem o valor de 3^13, porque B não
suporta declarações algébricas em suas variáveis. Por isso, colocamos a resposta da operação.
Outra função importante é PRINTF. Ela é uma função de saída para todos os �ns, que imprime
vários valores de acordo com uma string de formatação, lembrando que uma string é uma
cadeia de caracteres.
randnm () { 
 extrn ultimonum, embaralhar; 
 ultimonum = ultimonum * embaralhar; 
 retorn (ultimonum); 
} 
ultimonum {1}; 
embaralhar {1594323};
Há 5 strings de formatação simples:
Por exemplo:
Resultado: A soma de 9 e 4 é 13.
A função de Biblioteca mais direta para leitura de entrada de dados é GETCHAR.
A GETCHAR lê um caractere no formato ASCII – Código Padrão Americano para o Intercâmbio
de Informação – da unidade de entrada atual.
Uma chamada para GETCHAR geralmente tem o formato: x = getchar ();
"% c" – Caractere ASCII (códigos que representam os caracteres de seu teclado do
computador); 
"% d" – Número em decimal (base 10 - 0123456789)
"% h" – Caractere BCD (Decimal Codi�cado em Binário) 
"% o" – Número em octal (base 8 - 01234567)
"% s" – String ASCII (códigos que representam os caracteres de seu teclado do
computador)
printf ("A soma de% d e% d é% d.", 9,4,13);
Caso queiramos ver o ECO desse caractere que entramos, usamos a função PUTCHAR. Ela
emite os caracteres ASCII diferentes de zero de uma única palavra de máquina para a unidade
de saída atual.
A Notação B fornece suporte aos operadores aritméticos tradicionais [+-*/] sendo avaliados
em ordem normal de operação, portanto [* e /] antes de [+ e -], sendo que números
negativos também são suportados e também declarados de forma normal, ou seja [sinal de –
antes do número] por exemplo: -1, -345 etc.
Quando usamos operações com números em ponto �utuante, colocamos o operador # na
frente, ou seja #9 e o 9.0 e o contrário, ou seja, converter um número de ponto �utuante em
número inteiro seria ##9.0, seria 9.
Operadores relacionais são frequentemente usados para testar condições para [if] instruções,
[while] instruções, e assim por diante.
Os operadores relacionais inteiros são:
x = getchar (); 
 
putchar (x);
== igual a; 
!= diferente de; 
> maior que; 
< menor que;
Todos esses operadores realizam comparações de inteiros. Para comparações de ponto
�utuante, os operadores são iguais aos anteriores, porém precedidos por um #.
Todas as expressões relacionais têm um valor numérico. O valor é 1 se a relação for
verdadeira, e 0 se a relação for falsa.
Por exemplo: x = (k <z); atribui 1 a [x] se [k] for menor que [z] e 0 caso contrário.
Da mesma forma que na grande maioria das Linguagens e Notações de Programação, os
operadores relacionais são avaliados da esquerda para a direita após todos os operadores
aritméticos terem sido avaliados.
Por exemplo: x + y > k + z; é equivalente a: (x + y) > (k + z), sendo que os parênteses podem
ser utilizados também para alterar a ordem das operações conforme a lógica imposta e o
desejo do codi�cador.
Por exemplo: x + (y > k) + z.
Quanto aos operadores lógicos:
Quando eles compõem uma expressão, só serão avaliados após os operadores relacionais.
>= maior ou igual a;
<= menor ou igual a.
AND: '&&' é o "e" lógico; 
OR: '||' é o “ou” lógico; 
NOT: '!' é o “não” unário (1 verdadeiro; 0 falso como retorno). 
IFs e ELSEs podem ser aninhados de uma maneira muito direta:
Temos também o tratamento de loops na Notação B, utilizando
a declaração WHILE.
Vamos vê-la num exemplo em que leremos os inteiros positivos do dispositivo de entrada de
dados e apresentaremos a sua média. À medida que os inteiros são digitados, eles podem ser
separados por qualquer número de espaços em branco ou caracteres de nova linha [*n]. É o
ENTER do seu teclado. Quando for digitado um 0 “zero”, isso indica o �m da entrada de
dados.
maximodetres (x,b,c) { 
 if (x > y) { 
 if (x > z) return (x); 
 else return (z); 
 } 
 else { 
 if (y > z) return (y); 
 else return (z); 
 } 
} 
main() { 
 auto z, x, numero, somar, terminou; 
 somar = x = 0; 
 terminou = 0; 
 z = getchar(); 
 while (!terminou) { 
 while ( (z == ' ') || (z == '*n') ) 
 z = getchar(); 
 numero = 0; 
 while ( (z != ' ') && (z != '*n') ) { 
 numero = numero * 10 + (z - '0'); 
 z = getchar(); 
Cabem algumas explicações básicas:
Estamos apresentando esses exemplos para você perceber como a Notação B é semelhante à
Notação da Linguagem C pura. A ideia aqui não é ensinar a Linguagem, mas dar subsídios para
que você entenda o seu potencial como Notação. 
B é um Método de especi�cação formal que, graças a uma Linguagem adequada, permite
expressões altamente precisas das propriedades exigidas pelas especi�cações.
O desenvolvimento B:
 } 
 if (numero == 0) terminou = 1; 
 else { 
 x += 1; 
 somar += numero; 
 } 
 } 
 printf("Average = %d %d/%d*x",somar/n,somar%n,x); 
} 
O loop externo [while (!terminou)[ continuará a fazer o loop e obter números até
que um dos números obtidos seja [0] zero, lembra?!
O segundo loop [while ( (z == ' ') || (z == '*n') )] libera quaisquer espaços em
branco ou caracteres de nova linha na entrada. Quando encontra um caractere que
não é um espaço em branco nem uma nova linha, assume que encontrou o início
de um número; 
O terceiro loop [while ( (z != ' ') && (z != '*n') )] coleta o número da entrada. A
coleta do número é interrompida quando o loop encontra outro caractere em
branco ou de nova linha. 
Em suma, os objetivos da Notação B são:
Provavelmente você não deve ter tido contato com a Notação B, em muitos casos, devido a
você ainda não trabalhar ou atuar na indústria de software para uso comercial, web ou mobile,
mas saiba que B é muito utilizado na Indústria de forma geral e na de defesa, entre outras.
Vejamos quais são seus campos de aplicação:
Começa com a redação de um modelo concreto que inclui todas as necessidades
de�nidas;
Descrição dos principais dados processados pelo Sistema e as propriedades
fundamentais desses dados;
As funções garantem o processamento desses dados preservando suas
propriedades;
É então transformado, até que uma Notação completa do software seja obtida;
Isso gerará um modelo concreto, comprovado e sem falhas, que pode ser
codi�cado em alguma outra Linguagem de Programação. Preferencialmente em C,
como já vimos nos exemplos anteriores, devido à sua semelhança.
Criar software correto por construção;
Modelar Sistemas em seu ambiente;
Formalizar especi�cações;
Simpli�car a Programação.
Indústria: busca de Sistemas seguros que usem Métodos Formais, bem como
novas Tecnologias que atendam às suas necessidades;
Para você poder praticar a Notação B, mencionamos o link a seguir.
Clique no botão para conferir o conteúdo.
Empreendedores:  buscando respostas para questões funcionais e contando com o
Método B como solução sustentável;
Especialistas: indivíduos que buscam informações sobre Métodos Formais em
Nível Técnico muito alto;
Pesquisadores especializados em P&D (Pesquisa e Desenvolvimento):
trabalhando para o desenvolvimento sustentável de Métodos Formais a �m de
desenvolver novas soluções para o futuro.
Site 
A nova licença do Atelier B V4 é distribuída gratuitamente a todos
aqueles que pretendam utilizar o Atelier B para investigação, ensino e
desenvolvimento dos seus Projetos Industriais. Assim que a
ferramenta é usada pela primeira vez, ela é alocada por um tempo
ilimitado. A ferramenta é completa, tem Manuais e Cursos para quem
quiser praticar e saber mais. Lembre-se de que o Mercado está
competitivo e para se manter com alta empregabilidade, os
diferenciais entre os candidatos é visto normalmente no que um
conhece e foi além daquilo que todos os outros sabem por obrigação.
Invista em sua carreira.
ACESSE
Linguagem de Especi�cação Algébrica Comum 
Trata-se da CASL – The Common Algebraic Speci�cation Language (Linguagem de Especi�cação
Algébrica Comum).
É uma Linguagem expressiva para a especi�cação formal de requisitos funcionais e design
modular de software. 
Foi projetada pela COFI (Iniciativa de Estrutura Comum Internacional para Especi�cação e
Desenvolvimento Algébrico). É baseada em uma seleção crítica de recursos que já foram
explorados em vários contextos, incluindo subclassi�cações, funções parciais, lógica de
primeira ordem e especi�cações estruturadas e arquitetônicas:
“CASL é uma Linguagem de especi�cação expressiva que foi projetada para
substituir muitas linguagens de especi�cação algébrica existentes e fornecer um
padrão. CASL consiste em várias camadas, incluindo especi�cações básicas (não
estruturadas), especi�cações estruturadas e especi�cações arquitetônicas; os
últimos são usados para prescrever a estrutura modular das implementações.
Descrevemos uma versão simpli�cada da sintaxe CASL, semântica e cálculo de
prova para cada uma dessas três camadas e declaramos os teoremas de
integridade e integridade correspondentes. As camadas são ortogonais no sentido
de que a semântica de uma dada camada usa a da camada anterior como uma
https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/
O CoFI Language Design Group foi formado na reunião de fundação da Common Framework
Initiative, em Oslo, na Noruega, em 1995. Seu objetivo era propor uma estrutura comum que
fosse capaz de substituir muitas estruturas de especi�cação algébrica existentes. Um Projeto
Inicial do CASL foi proposto em 1997, cujo design foi �nalizado em abril de 1998 e a primeira
versão da Linguagem CASL foi lançada no �nal de 1998.
Foi projetada por um grande grupo de especialistas para uso prático no desenvolvimento de
software. Por se tratar de uma Linguagem Expressiva, é apropriada para especi�car requisitos
e design para pacotes de software convencionais. 
Como o próprio nome diz, ela é algébrica no sentido de que os seus modelos de especi�cações
são álgebras.
Algumas de suas partes são: 
Como bem sabemos, você já teve a oportunidade, em outros momentos de estudo, de aprender
os princípios dos operadores e os sinais utilizados em álgebra.
- MASSAKOWSKI et al., 2008, p. 1
Especi�cações básicas, para a especi�cação de Módulos de Software individuais;
Especi�cações estruturadas, para a especi�cação Modular de Módulos;
Especi�cações arquitetônicas, para a prescrição da Estrutura de Implementação;
Bibliotecas de especi�cações, para armazenamento de especi�cações.
“caixa preta”, e da mesma forma para os cálculos de prova. Em particular, isso
signi�ca que CASL pode ser facilmente adaptado a outros sistemas lógicos.”
Vamos colocar, aqui, 3 exemplos simples de declarações utilizando a Linguagem CASL para
que, utilizando aquelas tabelas, você consiga entender o signi�cado das expressões. 
A ideia aqui não é aprender a Notação e as regras todas, mas entender os princípios e
conseguir ao menos ler as expressões algébricas.
Mas antes, vamos relembrá-los aqui:
Tabela 1 – Símbolos Matemáticos Lógicos
Símbolo Nome do Símbolo
Signi�cado /
De�nição
Exemplo
– e e/and x – y
^
Acento circun�exo /
circun�exo
e/and x ^ y
& "e" comercial e/and x & y 
+ Mais ou/or x + y 
∨ 
Acento circun�exo
invertido 
ou/or x ∨ y 
| Linha vertical ou/or x | y 
x ' Citação única Não - negação x ' 
x Barra Não - negação x
Símbolo Nome do Símbolo
Signi�cado /
De�nição
Exemplo
¬ Não Não - negação ¬ x 
! 
Ponto de
exclamação 
Não - negação ! x 
⊕ 
Círculo mais /
oplus 
Exclusivo ou - xor x ⊕ y 
~ Til Negação ~ x 
⇒ Implica 
⇔ Equivalente 
Se e somente se
(i�) 
 
↔ Equivalente 
Se e somente se
(i�) 
 
∀ Para todos 
∃ Existe 
∄ Não existe 
∴ Portanto 
∵ Porque / desde 
Agora, vamos aos exemplos:
Figura 1 – Sintaxe CASL. A sintaxe CASL para declarações e
axiomas envolve Notação familiar, e é principalmente
autoexplicativa
Fonte: Reprodução
Figura 2 – Extensões de uma sintaxe CASL. As
especi�cações podem ser facilmente estendidas por novas
declarações e axiomas
Fonte: Reprodução
Figura 3 – Exemplo de um símbolo de operação (ou
predicado) que pode ser declarado e sua interpretação
pretendida de�nida ao mesmo tempo.
Fonte: Reprodução
 Flexibilizando o exemplo, temos outra apresentação possível (logo a seguir), porém mais
didática: 
Figura 4 – Uso de símbolos de operação em uma sintaxe
CASL. Em casos simples, um símbolo de operação (ou
predicado) pode ser declarado e sua interpretação
pretendida de�nida ao mesmo tempo
Fonte: Reprodução
Caso você tenha se interessado em CASL e na pureza algébrica de suas declarações, sugerimos
a leitura deste documento sobre os alicerces desta Linguagem. 
Este é um bom momento para você fazer isso e, de quebra, treinar a Linguagem mundial da
Tecnologia da Informação, o inglês.
Clique no botão para conferir o conteúdo.
ACESSE
VDM 
O Método de Desenvolvimento de Viena ou VDM é um ambiente para Modelagem e
Desenvolvimento de Sistemas de Software Sequenciais. A Linguagem de especi�cação do VDM
evoluiu do Meta-IV.
Trata-se de uma Linguagem usada no Laboratório de Desenvolvimento da IBM em Viena, para
especi�car a semântica da Linguagem de Programação PL/I no início dos anos 70 do século
XX.
A versão atual da Linguagem de Especi�cação VDM, VDM-SL foi padronizada pela
International Standards Organization, a ISO. Ela suporta a modelagem e análise de Sistemas de
Software em diferentes níveis de abstração que podem, ainda, ser re�nadas em um nível
inferior, para derivar um modelo concreto que está mais próximo da implementação �nal do
Sistema.
Na década de 80 do século XX, VDM experimentou uma mudança de uma Linguagem de
De�nição para um Método de Desenvolvimento. 
O Método tornou-se cada vez mais padronizado:
Leitura 
CASL: The Common Algebraic Speci�cation Language
https://www.academia.edu/13919095/CASL_The_Common_Algebraic_Specification_Language
"VDM-SL com todas as suas invariantes, pré-condições e pós-condições é uma Linguagem
muito complexa e altamente expressiva. Portanto, nem sempre é possível determinar
estaticamente se um modelo é consistente. Isso dá origem a obrigações de prova, ou seja,
condições que devem ser comprovadas para garantir a adequação do modelo. Um exemplo
para tal obrigação é a obrigação de satisfação: Uma operação deve produzir um resultado que
satisfaça a pós-condição para cada entrada que satisfaça a pré-condição. A obrigação de
satisfação para a operação DEQUEUE é assim:
Figura 5
Fonte: Reprodução
Uma prova para a condição acima em estilo é mostrada a seguir:
Figura 6
Fonte: Reprodução
A prova começa com a hipótese (from) e termina com a conclusão (infer). Entre essas duas
linhas cada etapa introduz uma nova de�nição, aplica várias regras ou combina outras linhas.
As justi�cativas à direita das linhas mostram quais regras foram aplicadas ou quais linhas
foram combinadas. Os números representam os números de linha da prova atual e [hn]
descreve a décima hipótese. Outras regras, como a regra de inferência para conjunção
mostrada a seguir, devem ser de�nidas em outro lugar" (MÜLLER, 2009, p. 8).
Mais uma vez, a ideia aqui é mostrar a existência da Notação e dar algum exemplo para que
você tenha referência.
Abstract State Machines
Os avanços na Teoria, o desenvolvimento de ferramentas e o emprego industrial progressivo
de Abstract State Machines – Máquinas de Estado Abstratas, conhecidas como ASM nos anos
1990 transformaram-nas em uma técnica prática rigorosa para a Disciplina de Engenharia de
Sistema em Geral. 
Embora a de�nição de ASM seja surpreendentemente simples, ela oferece um certo número
de Métodos teoricamente bem fundamentados e industrialmente úteis, que suportam todo o
ciclo de desenvolvimento de software e incluem Modelagem e Métodos de Análise como a
veri�cação Matemática e a validação experimental para:
O caráter operacional e abstrato das ASM:
Atuar nos requisitos: durante as fases iniciais de desenvolvimento de software,
apoiando sua elicitação, especi�cação, inspeção e teste por meio dos chamados
modelos de solo;
Re�nar os modelos de alto nível: por meio de um Processo de Design que conecta
de forma con�ável os requisitos ao Código, suportando uma Disciplina de
Documentação Prática para manutenção e a reutilização do Código.
Torna a �delidade das de�nições com relação às intenções do Projeto veri�cável
por inspeção direta;
Suporta, por re�namentos graduais, vinculando a de�nição de alto nível de forma
transparente à sua implementação, em que cada etapa de re�namento re�ete as
decisões de design que se deseja documentar para referência futura, portanto,
reutilização e manutenção por exemplo;
Fornece uma base conveniente para transformar as de�nições abstratas em
modelos executáveis que podem ser usados para validação e experimentos;
Uma ASM sequencial é de�nida como um conjunto de regras de transição, ou seja, [se]
condição, [então] atualizações, que transformam estruturas de primeira ordem, ou seja, os
estados da máquina, em que a [condição] de guarda deve ser satisfeita para que uma regra
seja aplicável, e [atualizações] é um conjunto �nito de atualizações de função contendo
apenas termos livres variáveis de forma que: f(t1, ..., tn):=t.
ANSI/ISO C Speci�cation Language 
A ANSI/ISO C Speci�cation Language ou ACSL é uma Linguagem de Especi�cação para
Programas C, usando pré e pós-condições e invariantes do estilo Hoare (que você já viu em
outros momentos desse nosso Curso), que segue o paradigma design by contract – design por
contrato. 
As especi�cações são escritas como comentários de Notação C para o Programa C que,
portanto, podem ser compilados com qualquer compilador C. A ferramenta de veri�cação atual
para ACSL é o Frama-C.
Frama-C é uma plataforma extensível e colaborativa de Código aberto dedicada à análise de
Código-fonte de software C. Os analisadores Frama-C auxiliam você em várias atividades
relacionadas ao Código-fonte, desde a navegação por Projetos desconhecidos até a
certi�cação de softwares críticos.
Simpli�ca a justi�cativa matemática da correção do projeto, oferecendo uma
estrutura rigorosa para a análise de propriedades de tempo de execução no nível
de abstração mais apropriado.
Clique no botão para conferir o conteúdo.
ACESSE
Clique no botão para conferir o conteúdo.
ACESSE
ACSL é uma Linguagem de Especi�cação de Interface Comportamental que tem como objetivo
especi�car as propriedades comportamentais do Código-fonte C. 
A seguir, temos um exemplo que mostra uma aplicação da regra de escolha em ACSL:
Site 
Conheça e estude mais sobre o Frama C acessando o link abaixo.
Leitura 
ASCL by Example 
No link a seguir você poderá estudar exemplos.
https://frama-c.com/html/get-frama-c.html
https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf.
Figura 7 – Aplicação da regra de escolha em ACSL
Fonte: GERLACH, 2020, p. 24
São características da Linguagem:
JAVA Modeling Language
O Java Modeling Language – JML é uma Linguagem de Especi�cação de Interface
Comportamental, que pode ser usada para especi�car o comportamento de Módulos Java. 
Fornecer especi�cações primitivas para cobrir os aspectos de baixo nível da
Linguagem de Programação C;
Permitir uma especi�cação precisa dos contratos de função. Isso torna a
especi�cação não apenas compreensível por um ser humano, mas também
manipulável por um analisador.
Além disso, como nem sempre uma especi�cação
completa é útil, o contrato pode ser parcial, dependendo do que se deseja veri�car;
Permitir um raciocínio mais abstrato por meio de tipos matemáticos ou lógicos,
ou por meio da de�nição de ideias de alto nível.
Ele combina a abordagem de design por contrato e a abordagem de especi�cação baseada em
Modelo de Linguagens de Especi�cação de Interface, com alguns elementos do re�no de
cálculo.
A interface do Método ou Tipo são as informações necessárias para usá-lo de outras partes de
um Programa. No caso de JML, esta é a sintaxe Java e as informações de tipo necessárias para
chamar um Método ou usar um campo ou tipo. 
Para um Método, a interface inclui coisas como o nome do Método, seus modi�cadores,
incluindo sua visibilidade, seu número de argumentos, seu tipo de retorno, quais exceções ele
pode lançar, e assim por diante. 
Para um campo, a interface inclui seu nome e tipo, e seus modi�cadores. 
Para um tipo, a interface inclui seu nome, seus modi�cadores, seu pacote, seja uma classe ou
interface, seus supertipos e as interfaces dos campos e Métodos que declara e herda. 
Fique claro que a Linguagem de especi�cação JML especi�ca todas essas informações de
interface, usando a sintaxe Java.
O comportamento de um Método ou tipo descreve um conjunto de transformações de estado
que ele pode realizar. 
O comportamento de um Método é especi�cado ao descrever: um conjunto de estados em que
a chamada do Método é de�nida, um conjunto de locais que o Método pode atribuir e,
portanto, alterar e as relações entre o estado de chamada e o estado em que ele retorna
normalmente, lança uma exceção ou pode não retornar ao chamador. 
Os estados para os quais o Método é de�nido são formalmente descritos por uma a�rmação
lógica, chamada de pré-condição do Método. 
As relações permitidas entre esses estados e os estados que podem resultar do retorno normal
são formalmente descritas por outra a�rmação lógica chamada de Pós-condição Normal do
Método. 
Da mesma forma, as relações entre esses pré-estados e os estados que podem resultar do
lançamento de uma exceção são descritas pela Pós-condição Excepcional do Método. 
Os estados para os quais o Método não precisa retornar ao chamador são descritos pela
condição de divergência do Método. No entanto, a especi�cação explícita de divergência
raramente é usada em JML.
Vamos ver um exemplo de Código para entendermos como funciona a declaração nessa
Linguagem.
Figura 8 – Especi�cação JML de uma classe abstrata Java
simples IntHeap
Fonte: cs.ucf.edu
Você deve ter percebido que como JML ainda não é o�cialmente suportada pelo Java, todas as
declarações JML devem ser escritas dentro de comentários. 
As instruções JML sempre se referem a uma classe Java especí�ca ou Método, portanto,
devem ser escritas dentro dos colchetes [] da classe principal. 
Quando se referem a um Método especí�co, devem ser escritos dentro dos colchetes [] do
Método logo a seguir da declaração.
Lembre-se de que JML segue o Paradigma de Programação Design-by-Contract, como escrevi
anteriormente.
Isso signi�ca que ela descreve as pré/pós condições do Código que devem ser respeitadas para
obter o comportamento correto e esperado. Então, sob um ponto de vista mais formal, avaliar
JML signi�ca veri�car se o código Java viola o contrato do Design-by-Contract.
Vamos a uma explicação desse exemplo:
“A interface dessa classe consiste nas linhas 1, 3, 15 e 18. A linha 3 especi�ca o
nome da classe e o fato de que a classe é pública e abstrata. As linhas 15 e 18,
além de seus comentários, fornecem as informações de interface para os
Métodos desta classe. O comportamento desta classe é especi�cado nas Notações
JML encontradas nos comentários especiais que têm um sinal de arroba ( @)
como seu primeiro caractere seguindo o início do comentário usual. Essas linhas
parecem comentários para Java, mas são interpretadas por JML e suas
ferramentas. Por exemplo, a linha 5 começa com um marcador de comentário de
Notação do formulário //@, e essa Notação continua até //próximo ao �nal da
linha, que inicia um comentário dentro da Notação que até mesmo JML ignora. A
- LEAVENS et al., 2006, p. 2
outra forma de tais Notações pode ser vista nas linhas 7 a 14, linha 17 e nas
linhas 15 e 18. Essas Notações começam com os caracteres /*@ e terminam com
@*/ou */; dentro de tais Notações, sinais de arroba (@) no início das linhas são
ignorados pelo JML. Observe que não pode haver espaço entre o início do
marcador de comentário, ou //ou /*e o primeiro símbolo de arroba; assim, //
@começa um comentário, não uma Notação. A primeira Notação, na linha 5 da
�gura acima, dá a especi�cação de um campo, denominado elements, que faz
parte da especi�cação comportamental desta classe. Ignorando, por enquanto, os
modi�cadores JML extras, deve-se pensar neste campo, em essência, como
sendo declarado como: elements public int []; Ou seja, é um campo público com
um tipo de array inteiro; dentro das especi�cações, é tratado como tal. No
entanto, por ser declarado em uma Notação, esse campo não pode ser
manipulado pelo código Java. Portanto, por exemplo, o fato de o campo ser
declarado público não é um problema, pois ele não pode ser alterado diretamente
pelo código Java. Essas declarações de campos nas Notações devem ser marcadas
como campos apenas de especi�cação, usando o modi�cador JML model. Um
campo de modelo deve ser pensado como uma abstração de um conjunto de
campos concretos usados na implementação desse tipo e seus subtipos. Ou seja,
imaginamos que os objetos que são instâncias do tipo [IntHeap] possuem tal
campo, cujo valor é determinado pelos campos concretos que são conhecidos por
Java no objeto real. Claro, em tempo de execução, objetos do tipo IntHeap não tem
tal campo, os campos do modelo são puramente imaginários. A especi�cação do
Método largest é dada nas linhas 7 a 15. A linha 7 diz que esta é uma
especi�cação pública de comportamento normal. JML permite várias
especi�cações diferentes para um determinado Método, que pode ter diferentes
níveis de privacidade. O modi�cador public diz que a especi�cação deve ser usada
por clientes. A palavra-chave normal_behavior informa ao JML várias coisas.
Primeiro, ele diz que a especi�cação é uma especi�cação de Método pesada, em
oposição a uma especi�cação de Método leve como a fornecida na linha 17.”
Vamos conhecer melhor as declarações: 
Fora isso, temos as ditas invariantes. Invariantes especi�cam condições que são satisfeitas no
início e no �nal de qualquer invocação de Método e no �nal da invocação do construtor.
Uma invariante pode ser pública ou privada, dependendo de qual tipo de variáveis e Métodos
ela usa (apenas pública => invariante pública, pelo menos uma invariante privada => privada). 
Elas não precisam ser mantidas durante a execução de um Método, mas podem ser
interrompidas temporariamente.
Predicative Progamming
//@assignable: lista de variáveis (divididas por vírgula) que podem mudar de valor
durante a execução do Método (= variáveis mutáveis). Se não houver variáveis
mutáveis na classe, use a palavra-chave reservada \nothing;
//@requires: pré-condições do Método;
//@ensures: pós-condições do Método;
//@signals: descreve uma exceção que o Método pode lançar e as condições nas
quais isso acontece;
//@pure: declara que o Método é um observador, o que signi�ca que não altera
nenhum valor das variáveis de classe. Nota: Métodos puros são implicitamente
//@assignable: \nothing;
//@also: o Método herda especi�cações de seus supertipos.
Primeiramente, devemos aclarar que no contexto da Ciência da Computação não estamos
interessados em declarar um fato, mas sim, em testar uma condição verdadeira/falsa, com o
propósito de decidir se devemos fazer algo. Um predicado como uma função que obtém
argumentos e retorna um booleano. Ele retorna verdadeiro se o argumento corresponder ao
predicado, isto é, o nome-�ltro da função.
Assim, um
predicado faz uma pergunta cuja resposta é verdadeira ou falsa ou, dito de outra
forma, sim ou não. 
Na Ciência da Computação e na Matemática, essa questão vem na forma de uma função. O
resultado da função é verdadeiro ou falso, sim ou não, 1 ou 0. 
O tipo de dados da resposta, novamente tanto na Matemática quanto na Ciência da
Computação, é chamado de booleano.
Por exemplo, se tivermos uma pergunta como: a temperatura é maior que 30 graus?
Podemos escrever: temperatura > 30.
A resposta é verdadeira, por exemplo, se a temperatura for 31 ou falsa, se a temperatura for 21.
Para escrevermos isso usando uma função Java, por exemplo, teríamos algo como: 
boolean checkTemperature(int temperature) 
{ 
 return temperature > 30; 
} 
Programação predicativa, como é conhecida, é o nome original de um Método Formal para
especi�cação e re�namento de programas, e foi criada por Eric Hehner. 
A principal Área de Pesquisa de Hehner (Cientista da Computação canadense) são os Métodos
Formais de design de software. Seu Método, inicialmente chamado de programação predicativa,
e mais tarde chamado de Teoria Prática da Programação, é considerar cada especi�cação
como uma expressão binária booleana, e cada construção de programação como uma
expressão binária que especi�ca o efeito da execução da construção de programação.
A ideia central é que cada especi�cação é uma expressão booleana verdadeira para os
comportamentos aceitáveis do computador e falsa para os comportamentos inaceitáveis.
Segue-se que o re�namento é apenas uma implicação. 
Este é o Método formal mais simples e o mais geral, aplicando-se a programas sequenciais,
paralelos, autônomos, comunicantes, terminantes, não terminados, em tempo natural, em
tempo real, determinísticos e probabilísticos e inclui limites de tempo e espaço.
Importante notar que nem sempre precisam usar números como retorno de predicados. 
Por exemplo, podemos �ltrar em um conjunto de animais:
 leão, elefante, papagaio, baleia, cavalo, águia, gato, cão, humano, pintassilgo, esquilo
Se quisermos criar um conjunto de pássaros, usaremos o predicado:
É um pássaro(animal) := verdadeiro se animal é um pássaro
E o conjunto �nal seria:
papagaio, águia, pintassilgo
 Como nós realmente programaríamos isso dependeria de nossa representação dos animais.
Por exemplo, poderíamos representar cada animal como um conjunto de valores em uma
matriz.
A seguir, temos um exemplo muito interessante utilizado em Lógica Difusa:
Figura 9 – Exemplo de predicado de Lógica Difusa
Fonte: Reprodução
 Assim:
“No diagrama, de�nimos um predicado IsItHot (T) que responde à pergunta,
“Está quente?”. Aqui, se IsItHot (T) = 1,0 , a resposta é “sim”, e se PIsItHot (T) =
0,0 , a resposta é “não”.
Na lógica booleana normal (verdadeiro / falso), vemos que há uma transição
abrupta entre quente e frio. Isso não corresponde à nossa intuição. Porém, o
predicado da lógica difusa tem uma transição lenta entre quente e frio. Quanto
mais próxima a resposta estiver de 1.0, mais quente está a água e, quanto mais
Notação Z
Z é uma Linguagem de Especi�cação Formal que torna mais fácil escrever descrições
matemáticas de Sistemas Dinâmicos Complexos, como softwares. 
As descrições são geralmente menores e mais simples do que qualquer Linguagem de
Programação pode fornecer:
- BLUROCK, 2020, p. 9
próximo de 0.0, mais fria está a água. Se o valor for 0.5, então não temos
certeza.”
“É uma Linguagem de especi�cação formal orientada para modelos que foi
proposta por Jean-Raymond Abrail, Steve Schuman e Betrand Meyer em 1977 e
foi mais tarde desenvolvida no grupo de pesquisa de programação da
Universidade de Oxford. É baseado na teoria dos conjuntos axiomáticos de
Zermelo Fränkel e na lógica predicada de primeira ordem. A Notação Z é uma
Linguagem de especi�cação fortemente digitado, matemático. Ele tem um
suporte de ferramenta robusto disponível comercialmente para veri�car textos Z
para sintaxe e erros de tipo da mesma forma que um compilador veri�ca o
código em uma Linguagem de programação executável. 
Não pode ser executada, interpretada ou compilada em um programa em
execução. Permite que a especi�cação seja decomposta em pequenos pedaços
chamados esquemas. O esquema é a principal característica que distingue Z de
outras Notações formais. Em Z, aspectos estáticos e dinâmicos de um sistema
Z é composta de duas linguagens:
Esquemas são uma estrutura que lembra uma caixa, em que se introduz variáveis e se
especi�ca a relação entre essas variáveis. 
Figura 10 – Exemplo de Estrutura em Z
Fonte: Exemplo de Estrutura em Z
- RUHELA, 2012, p. 4
Linguagem Matemática: é usada para descrever vários aspectos de um design:
objetos e as relações entre eles usando lógica proposicional, lógica predicada,
conjuntos, relacionamento e funções;
Linguagem de Esquema: é usada para estruturar e compor descrições: coletar
informações, encapsulá-las e nomeá-las para reutilização.
podem ser descritos usando esquemas. A especi�cação Z descreve o modelo de
dados, o estado do sistema e as operações do sistema. A especi�cação Z é útil
para quem elicita os requisitos, aqueles que implementam programas para
atender a esses requisitos, aqueles que testam as consequências e aqueles que
escrevem manuais de instrução para o sistema.”
Figura 11 – Exemplo de uma declaração em Z
Fonte: csm.ornl.gov
Observe que todas as declarações são feitas acima da linha central e os predicados são
de�nidos a seguir da linha central.
Clique no botão para conferir o conteúdo.
Leitura 
A Linguagem de Especi�cação Z 
Para podermos caminhar e conhecer um pouco melhor essa Notação.
Sugerimos a leitura do resumo na forma de apresentação construído
por: CARREIRA, L. A Linguagem de especi�cação Z. 2014.
ACESSE
Vamos utilizar essa base para alguns exercícios.
https://slideplayer.com.br/slide/384264/
Indicações para saber mais sobre os assuntos abordados
nesta Unidade:
  Sites  
ACSL Language  
Para quem quer aprender mais sobre a Linguagem ACSL, temos o Git da página o�cial da
Linguagem, Manuais, exemplos e demais itens que, ceramente interessarão ao codi�cador.
Explore o repositório e aprenda mais. 
Clique no botão para conferir o conteúdo.
ACESSE
  Vídeo  
Linguagens Formais e Autômatos: Conteitos Iniciais
2 / 3
˨ Material Complementar
https://github.com/acsl-language/acsl/
  Leitura  
User Manual 
BIDOIT, M.; MOSSES, P. D. CASL – User Manual. Nova Iorque, USA. 2004.
Clique no botão para conferir o conteúdo.
ACESSE
The Z Notation: A Reference Manual 
SPIVEY, J. M. The Z Notation: A Reference Manual. UK: Prentice Hall International Ltd., 1998.
Clique no botão para conferir o conteúdo.
ACESSE
linguagens formais e autômatos: conceitos iniciais.
http://www.informatik.uni-bremen.de/cofi/CASL-UM.pdf
https://www.cs.umd.edu/~mvz/handouts/z-manual.pdf
https://www.youtube.com/watch?v=iNkT-K0mH7w
BLUROCK, E. Predicados em Ciência da Computação. 2020.
GERLACH, J. ACSL by Example. Alemanha: Fraunhofer-Fokus, 2020.
LEAVENS, G. T.; BAKER, A. L.; RUBY, C. Preliminary design of JML: a behavioral interface
speci�cation language for Java. 2006.
MASSAKOWSKI, T. et al. Casl – A Linguagem Comum de Especi�cação Algébrica. 2008.
MÜLLER, A. VDM – The Vienna Development Method. 2009.
RUHELA, V. Z. Formal Speci�cation Language – An Overview. International Journal of Engineering
Research & Technology – IJERT, India, v. 1, issue 6, p. 4, Aug. 2012.
3 / 3
˨ Referências