/* 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 08: Pilha via Vetor com Interface */ /* Tendo realizado uma implementação de pilha que expunha os detalhes de implementação para o usuário da estrutura, nós vamos agora refinar a implementação, de forma a separar os elementos da interface de pilha dos elementos que dizem respeito à implementação de pilha usando vetor. Nós usaremos, para a especificação de interfaces, o recurso de "traits" de Dafny. */ /* EXERCÍCIO 1: Leia a introdução a "traits" do capítulo 13 da referência de Dafny https://github.com/Microsoft/dafny/blob/master/Docs/DafnyRef/out/DafnyRef.pdf Em seguida, defina um trait "Pilha", cujos campos devem conter os elementos essenciais para a especificação de uma pilha com limite de tamanho e de elementos inteiros. Exemplos: - O tamanho máximo da pilha: esse valor é recebido na inicialização. - Uma sequência de inteiros, para especificar convenientemente os elementos empilhados. - Um "set", que podemos chamar de "representação", para especificar, de forma abstrata, o conjunto dos objetos que serão manipulados pelos métodos de pilha (esse conjunto será mencionado, portanto, nas cláusulas "modifies" desses métodos). IMPORTANTE: todos os membros acima devem ser declarados como "ghost", indicando que eles fazem parte apenas da especificação, e portanto que não precisam fazer parte do programa compilado. */ /* EXERCÍCIO 2: Dentro do trait "Pilha", adicione um predicado "valida". Ele não deve possuir corpo, indicando que os detalhes de o que significa uma representação de pilha estar válida dependem da representação, e que portanto não podem estar na interface. Esse predicado pode, porém, conter elementos de especificação. Por exemplo, você provavelmente vai querer adicionar uma cláusula "reads" informando que esse predicado acessa tanto o objeto em questão (this) quanto os demais objetos que fazem parte da representação da pilha (o terceiro dos campos mencionados no exercício anterior). */ /* EXERCÍCIO 3: Escreva agora os predicados "cheia" e "vazia", incluindo o corpo dos predicados. Observe que esses predicados podem ser escritos de forma independente de como a pilha será implementada: basta fazer menção à sequência de inteiros que especifica os elementos empilhados, etc. */ /* EXERCÍCIO 4: Escreva agora as declarações dos métodos "inicializar_como_vazia", "empilhar" e "desempilhar". Você não deve fornecer os corpos desses métodos, pois eles dependem da implementação de pilha, mas deve fornecer, em termos dos elementos de especificação da pilha, pré- e pós-condições que descrevam o comportamento adequado desses métodos. */ /* EXERCÍCÍO 5: Escreva agora uma classe como "Pilha_via_Vetor", estendendo o trait Pilha. Essa classe deve possuir os campos "concretos" (isto é, não "ghost") necessários para a implementação de pilha via vetor, por exemplo aqueles que você usou na implementação anterior de pilha. */ /* EXERCÍCIO 6: Escreva o predicado "valida", dessa vez incluindo o corpo do predicado, o qual deverá, em particular, relacionar os elementos da interface de pilha (por exemplo a sequência que especifica os elementos empilhados) e os elementos da implementação de pilha via vetor (por exemplo o vetor de inteiros). Observe que os predicados "cheia" e "vazia" não precisam ser escritos nesta classe, pois eles já estão completamente definidos na interface de pilha. */ /* EXERCÍCIO 7: Escreva agora o método "inicializar_como_vazia" de Pilha_via_Vetor. Em princípio, ele pode possuir a mesma especificação presente na interface de pilha, mas deve possuir também um corpo fornecendo a implementação do método. IMPORTANTE: a) Naturalmente, o corpo do método deve inicializar os elementos da implementação de pilha via vetor. Porém, ele deve inicializar também os campos "ghost" da interface! Isso significa que você terá inicializar o inteiro "tam_max", a sequência que especifica os inteiros empilhados e o conjunto dos objetos que constituem a representação de pilha. (Os demais métodos deverão manter esses campos atualizados.) b) É importante que, tanto na classe Pilha_via_Vetor quanto na interface Pilha, haja uma pós-condição garantindo que todos os objetos que estão no campo "representação" são "fresh", exceto "this", caso você tenha optado por incluir "this" no campo em questão. Essa garantia é crucial para que um usuário da pilha, ao chamar os métodos de pilha, saiba que tais métodos podem até alterar a representação de pilha, mas não alterarão outros objetos (justamente porque, pela restrição em questão, a representação da pilha é garantida ser composta apenas de objetos "novos", isto é, alocados pelos métodos de pilha -- exceto, como mencionado, pelo objeto "this). */ /* EXERCÍCIO 8: Escreva agora os métodos "empilhar" e "desempilhar" da classe Pilha_via_Vetor, nos mesmos moldes do método anterior. Em particular, com relação ao campo de "representação" da pilha, é importante garantir que todo objeto que está nesse campo ao fim desses métodos, mas que não estava no início da chamada ao método, foi alocado na chamada em questão. (Certamente, na implementação em questão de pilha via vetor, os métodos "empilhar" e "desempilhar" não fazem alocação nenhuma, e portanto você poderia escrever simplesmente que a "representação" é a mesma antes e depois da chamada do método. Porém, a versão anterior, menos restritiva, é útil por exemplo numa implementação por lista encadeada, em que o método "empilhar" de fato aloca um novo nó para a pilha.) */ /* EXERCÍCIO 9: Por fim, adapte o método que inverte um vetor utilizando uma pilha: agora, ele deve possuir uma variável do tipo Pilha, a qual deve ser inicializada com um objeto do tipo Pilha_via_Vetor. Você deve reescrever os invariantes desse método de forma a fazer uso apenas dos elementos presentes na interface de pilha. Você deverá notar que os invariantes ficam mais "limpos", pois mencionarão apenas a representação "abstrata" da pilha. Em particular, se resolvêssemos trocar a implementação via vetor por uma via lista encadeada, os invariantes permaneceriam os mesmos, e apenas a linha da alocação da pilha precisaria ser alterada. */