/* UNIVERSIDADE FEDERAL DO CEARÁ – DEPARTAMENTO DE COMPUTAÇÃO VERIFICAÇÃO DEDUTIVA DE PROGRAMAS – 2017.1 * Professor: Pablo Mayckon Silva Farias * Página: http://lia.ufc.br/~pmsf/2017-1/vdp/ AULA PRÁTICA 07: Classes em Dafny. */ /* Tendo estudado os recursos básicos de Dafny para a verificação de programas envolvendo vetores, nós agora estudaremos os recursos para a escrita e a verificação de programas envolvendo registros ou estruturas, utilizando para isso o recurso de classes de Dafny (mas sem interesse, por ora, em orientação a objetos). Nós utilizaremos como motivação prática a implementação e o uso de pilhas armazenadas em vetores. O restante deste arquivo contém as instruções para a realização da tarefa. Observação: a implementação sugerida abaixo expõe os detalhes da implementação da pilha para o usuário. A ideia é realizar uma primeira implementação dessa forma e observar as consequências ao utilizar a pilha. Na prática seguinte, nós faremos uma implementação que separe melhor a interface da implementação. */ /* EXERCÍCIO 1: Utilizando a sintaxe ilustrada no cap. 12 da referência de Dafny https://github.com/Microsoft/dafny/blob/master/Docs/DafnyRef/out/DafnyRef.pdf defina uma classe "Pilha" (*), incluindo um vetor de inteiros para armazenar os elementos da pilha e o que mais você precisar para manter o estado da pilha. Os métodos da classe serão escritos nos demais exercícios. ( * : Aqui e a seguir, os nomes apresentados nos enunciados são apenas sugestões; fique à vontade para escolher nomes diferentes.) */ /* EXERCÍCIO 2: Dentro da sua classe, escreva um predicado "valida". Ele deve exprimir condições para que a pilha esteja num estado válido; por exemplo, você pode exigir que o tamanho do vetor utilizado na representação seja pelo menos 1. Esse predicado será usado nas pré- e pós-condições dos métodos da pilha, de forma a garantir que eles sempre deixam o objeto em um estado válido. */ /* EXERCÍCIO 3: Escreva um método "inicializar_como_vazia", que receba como argumento um inteiro "tam_max". O método deve então deixar o objeto num estado que represente uma pilha vazia, pilha essa capaz de armazenar até "tam_max" inteiros. Escreva pré- e pós-condições definam a especificação do método. Em particular, as pós-condições devem garantir que o estado da pilha ao final do método é válido, chamando o predicado escrito anteriormente. */ /* EXERCÍCIO 4: Escreva um predicado "cheia", que exprima, em termos da representação da pilha, que a pilha está cheia. */ /* EXERCÍCÍO 5: Escreva um método "empilhar", que receba um inteiro e o coloque no topo da pilha. O método deve ter entre as pré-condições a exigência de que o estado da pilha é válido de início, e também que ela não está cheia. As pós-condições do método devem garantir que o conteúdo da pilha ao final consiste no que havia antes adicionado do novo elemento. Por simplicidade, você pode exprimir isso em termos de uma sequência, como em "a sequência final consiste na sequência inicial adicionada do novo elemento"; isso pode ser facilmente escrito em termos do vetor que é utilizado para a representação da pilha. Lembre que, ao final, a pilha também deve estar num estado válido. */ /* EXERCÍCIO 6: Escreva um predicado "vazia", para informar se a pilha está vazia. */ /* EXERCÍCIO 7: Escreva um método "desempilhar", que, desde que a pilha não esteja vazia, retorne o elemento do topo da pilha. Lembre de escrever pós-condições que forneçam as devidas garantias sobre o estado final, por exemplo relacionando os elementos antes e depois da operação. */ /* Feitos os exercícios anteriores, tem-se em mãos uma implementação básica de pilha, que pode então ser utilizada como parte de outro código a ser verificado. Essa é uma parte importante do processo de verificação de uma estrutura de dados, pois confirma que a especificação da estrutura permite que ela seja utilizada com sucesso (ou então mostra problemas concretos a serem sanados). */ /* EXERCÍCIO 8: Fora da classe "Pilha", escreva um método que receba um vetor de inteiros e cujas pós-condições garantam que, ao final do método, o vetor está invertido (o último elemento na primeira posição, etc). Para implementá-lo, você deve usar a sua classe "Pilha", da seguinte maneira: 0. Caso a sua estrutura de pilha não permita "tam_max" igual a zero, você pode começar tratando separadamente o caso em que o vetor a ser invertido tem tamanho 0. Não descarte, porém, o caso de tamanho 1, para que esse caso entre na parte do código que utilizará a pilha, aumentando o número de contextos que em que a estrutura será utilizada. 1. Em seguida, crie uma pilha com espaço suficiente para "n" números, sendo "n" o tamanho do vetor a ser invertido. 2. Em seguida, percorra o vetor a ser invertido, do início para o fim, colocando os elementos na pilha durante o processo. 3. Por fim, desempilhe "n" vezes, colocando os números desempilhados no vetor, novamente do início para o fim (dessa forma, o último elemento do vetor passará a ficar na primeira posição, etc). Observações importantes para a verificação desse método: a) A cláusula "modifies" desse método deve incluir apenas o vetor a ser invertido. Isso gera uma dificuldade, pois é o caso que o método cria e manipula outros objetos: o objeto da pilha, o vetor da pilha, etc. Intuitivamente, porém, não existe problema, pois esses objetos adicionais são todos objetos que foram alocados dentro do próprio método (ou seja, não existe risco de esse método alterar outros objetos alocados anteriormente). Esse argumento é suficiente para o sistema Dafny, mas de vez em quando você precisará lembrar ao sistema que esse é o caso, dizendo algo como "fresh(o)", isto é, "o objeto 'o' foi alocado durante a chamada em questão". Em particular, você deverá incluir entre as pós-condições do método "inicializar_como_vazia" a garantia de que o vetor da pilha é "fresh". b) Uma observação simples, mas que às vezes passa despercebida, é que métodos como "empilhar" e "desempilhar" podem até mudar os valores contidos no vetor da pilha (e etc), mas não modificarão o valor do ponteiro que aponta para esse vetor, etc. Esse tipo de pós-condição deve estar nos métodos da classe pilha, pois em caso contrário o verificador terá dificuldade em reconhecer, por exemplo, que, quando nós empilhamos um valor, nós podemos até mexer no vetor da pilha, mas não mexemos em outros vetores (por exemplo no vetor a ser invertido pelo método desta questão). c) Lembre que pode até ser que o verificador saiba de uma informação no início de um laço, e que o laço não altere a validade dessa informação, mas que a maneira padrão de lembrar esse fato ao verificador é usar um invariante. d) Se você seguiu as instruções acima, a verificação do método para inverter um vetor pode acabar mencionando bastante os detalhes de implementação da pilha, ao ponto inclusive de ficar evidente que teria sido muito mais simples usar diretamente um mero vetor auxiliar. Não se preocupe: o objetivo desta prática é apenas introduzir a manipulação de classes por meio de um exemplo concreto. A ideia é que, na prática seguinte, nós possamos produzir uma implementação de pilha que separe melhor a interface de pilha da implementação por meio de um vetor. */