Métodos Formais
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 1
Métodos Formais
São técnicas baseadas em formalismos
matemáticos para a especificação,
desenvolvimento e verificação dos sistemas de
softwares e hardwares.
Na Ciência da Computação...
... o termo método formal foi restrito para o uso de
notação formal para representar modelos de
©Ian Sommerville - Software Engineering
– TraduçãoProf
Pedro Fernandes -o
Métodos
Formais, 6o Períodode
Slide 2
sistemas
durante
processo
Métodos Formais

Não se tornaram as principais técnicas de
desenvolvimento de software
•
•
•
•
•
Outras técnicas foram utilizadas que resultou em melhorias na
qualidade do software.
O time-to-market é preferível.
O escopo de métodos formais é limitado.
A formalização é bem sucedida em domínios restritos ou
organizados.
No desenvolvimento de software não se pode validar
resultados apenas provando teoremas.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 3
Benefícios de Métodos Formais






Usados para reduzir o número de erros do
sistema.
Reduz tempo de desenvolvimento.
Proporciona melhor documentação.
Melhora a comunicação (entre equipe com o
usuário).
Facilita manutenção.
Ajuda a organizar as atividades durante o ciclo
de vida.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 4
Métodos Formais



Especificação Formal.
Análise e prova da especificação.
Verificação do programa.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 5
Especificação Formal
É uma especificação expressa em uma
determinada linguagem cujo vocabulário, sintaxe
e semântica são formalmente definidos e rígidos.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 6
Especificação Formal

Especificação vs. Implementação
–

O quê? vs. Como?
Especificações formais vs. especificações
informais
–
Formais: A notação utilizada possui uma sintaxe e uma
semântica totalmente precisa
–
Informal: Escritas em linguagem natural
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 7
Especificação Formal

Uma especificação formal provê:




Uma notação (domínio sintático);
Um universo de objetos (domínio semântico);
Regra precisa que define que objetos satisfazem cada
especificação.
Uma especificação é uma sentença escrita em
termos de elementos do domínio sintático.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 8
Especificação Formal

Uma linguagem de especificação é uma tripla
<Sin, Sem, Sat>:



Sin e Sem são conjuntos.
Sat é uma relação entre Sin e Sem.
Se Sat(sin, sem), então sin é uma especificação de sem, e
sem é um especificando de sin.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 9
Domínio Sintático

Definido em termos de:




um conjunto de símbolos (por exemplo, constantes,
variáveis e conectores lógicos).
Um conjunto de regras gramaticais para combinar esses
símbolos.
Necessidade de sentenças bem formadas.
O domínio sintático não se restringe a um
formato textual. Pode-se usar elementos
gráficos.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 10
Domínio Semântico


As linguagens de especificação diferem na
escolha do domínio semântico.
Exemplos:



Linguagens de especificação de tipos abstratos de dados.
Linguagens de especificação de sistemas distribuídos e
concorrentes.
Linguagens de programação.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 11
Propriedades de uma
Especificação

Não ambigüidade:


Consistente:


Deve ter uma interpretação semântica significativa.
Completa:


Cada especificação é mapeada em exatamente um
especificando.
A coleção de propriedades especificadas deve ser
suficiente para estabelecer compatibilidade com
especificações de mais alto nível.
Mínima
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 12
Especificação no Processo de
Software
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 13
Custo do Processo de Software
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 14
Técnicas de Especificação

Algébrica
–

O sistema é descrito em termos de operações e
relacionamentos entre elas.
Baseada em modelo
–
Um modelo do sistema é construído usando construções
matemáticas tais como conjuntos e seqüências e as
operações são definidas em termos de como elas alteram o
estado do sistema.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 15
Linguagens de Especificação
Formal
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 16
Estrutura de uma Especificação
Algébrica
< Nome da Especificação>
sort
< nome >
imports
< LISTA DE NOMES DA ESPECIFICAÇÃO>
Descrição informal do sort e de suas operações
Assinaturas de operação, que estabelecem os nomes e os
tipos de parâmetros às operações definidas sobre o sort
Axiomas que definem as operções sobre o sort
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 17
Componentes da Especificação

Introdução
–

Descrição
–

Descreve informalmente as operações
Assinatura
–

Define o sort (o nome do tipo) e declara outras
especificações que são usadas
Define a sintaxe e seus parâmetros
Axioma
–
Define a semântica das operações
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 18
Especificação algébrica
sistemática






Estruturação da especificação
Nomeação da especificação
Seleção da operação
Especificação informal de operação
Definição da sintaxe
Definição dos axiomas
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 19
Especificação de uma Lista
LISTA( Elem )
sort Lista
imports
INTEIRO
Define uma lista em que elementos são adicionados ao seu final e
removidos de seu início. As operações são CREATE, que busca uma
lista vazia; CONS, que cria uma nova lista com a adição de um membro;
Length, que avalia o tamanho da lista; HEAD, que avalia o primeiro
elemento da lista; eTAIL, que cria uma lista removendo o HEAD de sua
lista de entrada. UNDEFINED representa um valor indefinido do tipo Elem.
Create → List
Cons(List,Elem) → List
Head(List) → Elem
Length(List) → Inteiro
Tail(List) → List
Head(Create) = Undefined exception (empty List)
Head(Cons(L,v)) = if L=Create then v else Head(L)
Length(Create) = 0
Length(Cons(L,v)) = Length(L) + 1
Tail(Create) = Create
Tail(Cons(L,v)) = if L=Create then Create else Cons(Tail(L),v)
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 20
Especificações recursivas


Operações são frequentemente especificadas
recursivamente
Tail (Cons (L, v)) = if L = Create then Create
else Cons (Tail (L), v)
•
•
Cons ([5, 7], 9) = [5, 7, 9]
Tail ([5, 7, 9]) =
•
•
•
•
•
•
•
Tail (Cons ( [5, 7], 9)) =
Cons (Tail ([5, 7]), 9) =
Cons (Tail (Cons ([5], 7)), 9) =
Cons (Cons (Tail ([5]), 7), 9) =
Cons (Cons (Tail (Cons ([], 5)), 7), 9) =
Cons (Cons ([Create], 7), 9) =
Cons ([7], 9) = [7, 9]
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 21
Especificações recursivas
(*Funcao adiciona um item na lista,
ListDadoTempo*)
fun adic(item,[]) = [item]
| adic(item,item1::lista) =
[item]^^([item1]^^lista);
(*Funcao adiciona um item na lista,
ListDadoTempoS*)
fun adic1((item,tsr,s),[]) = [(item,agora(),s)]
|
©Ian Sommerville
- Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 22
adic1((item,tsr,s),(item1,tsr1,sn)::ListdadotempoS
Especificações recursivas
(*Funcao retira um item da lista, ListDadoTempoS*)
fun retira([]) = 0 |
retira((S1,item1,tsr)::lis) =
item1;
fun retira1([]) = 0 |
retira1((item1,tsr,s)::lis) =
Tsr;
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 23
Especificações recursivas
(*Funcao que define a capacidade maxima de
armazenamento do sensor*)
(*A lista eh invertida (rev), depois eh retirado o 1o
elemento dela (tl) e depois ela eh invertida mais
uma vez pra voltar a ordem original*)
fun
memoria(list:ListDadoTempoS):ListDadoTempoS
=
if length(list) > 8
then rev(tl(rev(list)))
else
list;
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período
Slide 24