Estrutura de um ficheiro de especificação

Um ficheiro de especificação contém normalmente três partes:

• Declarações. Servem para definir novos tipos, variáveis auxiliares, regras de reescrita ou abreviaturas.
• Axiomas. Lista de propriedades temporais assumidas pelo STeP numa sessão de verificação. Podem ser independentemente activados ou desactivados.
• Propriedades. Fórmulas temporais que se pretendem provar.

Na sua versão mais reduzida, um ficheiro de especificação pode conter apenas uma fórmula que será, por omissão, o objectivo da prova. Caso se pretendam definir vários objectivos então é necessário definir uma secção de propriedades, composta por um conjunto de linhas da forma:

PROPERTY nome da propriedade : fórmula temporal

Os axiomas são definidos de acordo com a seguinte sintaxe:

AXIOM nome do axioma : fórmula temporal

A secção de declarações pode ser usada para especificar as seguintes entidades:

• Abreviaturas para tipos, recorrendo à seguinte sintaxe:
  type id = tipo
• Novos datatypes.
• Funções não interpretadas (i.é, sem corpo). A sua declaração é feita da seguinte forma:
  value [atributo] id : [tipo ->] tipo
  O atributo (opcional) pode ser COMMUTATIVE, se a função for comutativa, ASSOCIATIVE, se a função for associativa, ou AC se for comutativa e associativa.
• Abreviaturas para funções. Na sua versão mais simples poderá ter a seguinte sintaxe:
  macro id = expressão
  Na sua expressão mais complexa, corresponde a uma declaração do tipo value seguida de uma clausula where onde é descrita a expansão sintática correspondente. Neste caso temos a seguinte sintaxe:
  macro id : [tipo ->] tipo where id = expressão
• Variáveis auxiliares. As variáveis podem ser rígidas, se o seu valor não se modificar ao longo do tempo, ou flexíveis, caso o contrário se verifique. A declaração de variáveis faz-se de acordo com a seguinte sintaxe:
  variable id, ..., id : tipo [espécie]
  A espécie pode ser Rigid ou Flexible. Quando omitida, as variáveis são declaradas como rígidas.

Um possível ficheiro de especificação para o programa da figura 1.1 é apresentado na figura 2.1.

  

Figure 2.1: Exemplo de ficheiro de especificação

SPEC

value COMMUTATIVE gcd : int*int --> int 

AXIOM gcd1: []Forall m,n:int . (m != n --> gcd(m,n) = gcd(m-n,n))

AXIOM gcd2: []Forall m:int . (m > 0 --> gcd(m,m) = m)
AXIOM gcd3: []Forall m:int . (m < 0 --> gcd(m,m) = -m)

PROPERTY aux1: [](y1 > 0)
PROPERTY aux2: [](y2 > 0)
PROPERTY aux3: [](gcd(y1,y2) = gcd(a,b))

PROPERTY part-corr: l8 ==> g = gcd(a,b)

Sempre que o ficheiro de especificação contenha mais do que uma única fórmula, deve começar pela palavra reservada SPEC. Tal como nos ficheiros SPL, os comentários fazem-se utilizando o caracter %, para indicar um comentário que só vai até ao fim da linha, ou usando (* e *) para um comentário que ocupe várias linhas. A extensão mais usada para estes ficheiros é .spec. Para ler um ficheiro de especificação para o STeP utiliza-se a opção Load specification do menu File.