Please enable JavaScript.
Coggle requires JavaScript to display documents.
Métodos Formais (Introdução a Máquinas Abstratas (Variáveis (armazena…
Métodos Formais
Introdução a Máquinas Abstratas
Variáveis
armazena informações
Invariantes
propriedades do estado válidas durante toda a execução
Operações
podem alterar o valor de variáveis ou não
O que é uma Máquina Abstrata
uma especificação de um sistema ou de parte de um sistema
Inicialização
estado inicial da máquina abstrata
Interface
coleção de operações
Pré-Condições mais Fracas
O que é?
Espaço de Estados
Coleção de todos os possíveis estados que uma máquina pode possuir
Dado uma coleção de variáveis, associadas com seus tipos, os possíveis estados associados a essas variáveis são simplesmente as possíveis combinações de valores que essas variáveis podem possuir
Exemplos
O espaço de estado de duas variáveis do tipo natural são todos os possíveis pares para os números naturais.
o espaço de estado de uma variável que está contida em um conjunto A é as partes do Conjunto de A
Notação
[S]P
Se P é um predicado, então ele é tratado como uma
pós-condição
de S, isto é, ele deve ser verdadeiro após a execução de S
Indica que o predicado P é verdadeiro para qualquer estado inicial onde o comando S chega a P com certeza. Isto é, quando executar S em um determinado estado e for garantido alcançar um estado final onde P é verdadeiro
indica uma condição sobre os estados antes da execução, ou seja, é uma
pre-condição
Quando
[S]P
é verdadeiro para todos os estados nos quais é garantido alcançar P, então temos a
Condição Mais Fraca de S para alcançar P.