A verificação de um programa tem como objetivo garantir que ele está correto segundo a sua especificação, ou seja, que produz o comportamento esperado para entradas válidas. Vale notar que isso não implica, necessariamente, que o programa resolva o problema do cliente (isso é validação). A verificação pode ocorrer por meio de testes representativos ou pela demonstração de correção formal.
- Testes: utilizam um conjunto de dados representativos como entrada e verificam se as saídas correspondem às esperadas. São úteis para confirmar o funcionamento prático do código.
- Demonstração de correção: aplica lógica formal (lógica de Hoare, predicados, e ter Conselhos de prova) para demonstrar que, para toda entrada que satisfaça a pré-condição, o programa satisfaz a pós-condição.
Um recurso central dessa abordagem são as asserções: predicados que descrevem condições que devem ser verdadeiras em pontos específicos do código. Cada trecho do programa é acompanhado por uma tripla de Hoare da forma {P} Código {Q}, onde P é a pré-condição, Q é a pós-condição esperada após a execução do código, e o código modifica as variáveis de acordo com essa relação.
Exemplo simples: se desejamos que, para toda entrada x > 0, exista uma saída y com y^2 = x, o código que gera y a partir de x deve manter a relação entre essas variáveis. Em termos da tripla de Hoare, teríamos algo como {x > 0} y := sqrt(x) {y^2 = x}, que expressa a correção condicional para esse trecho.
Observação: a verificação por tripla de Hoare olha o código de forma segmentada, de forma que cada trecho possui uma asserção que garante que, se a pré-condição for verdadeira, a pós-condição esperada será verdadeira após a execução desse trecho.
Observação prática: para demonstrar a correção de um trecho de código com atribuições, é comum olhar de trás para frente (em várias fontes, inclusive no material da disciplina), verificando quais condições devem ser verdadeiras depois da execução para que as condições anteriores sejam satisfeitas.
Dica: ao trabalhar com condições condicionais (if-else), é preciso demonstrar a correção de cada ramificação separadamente, assegurando que, em ambos os caminhos, a pós-condição desejada seja atingida.
Como referência prática, os itens a seguir apresentam uma linha de raciocínio típica para demonstrações de correção:
Resumo rápido do conceito de tripla de Hoare: {P} C {Q}, onde P é a condição anterior à execução de C, e Q é a condição que deve valer após C, para todo estado que satisfaz P.
Exercício rápido de verificação por trás para um trecho simples de código: se X := X - 2 deve levar a X = 3, requer P = (X - 2) = 3, isto é, X = 5, para o caso inicial que satisfaça a pré-condição.
Observação final: o objetivo total da demonstração é cobrir todo o trecho do código com triplas consistentes, de modo que a verificação se sustente para todas as execuções que satisfaçam as pré-condições.
Observação: a demonstração de correção costuma trabalhar com a análise de trechos de código isolados e, a partir deles, compor a verificação do programa como um todo.
Resposta correta: C) Verificação busca assegurar que o programa segue suas especificações, por meio de testes ou demonstração de correção.
Justificativa: verificação foca em confirmar que o código está conforme especificações técnicas; validação verifica se atende às necessidades do usuário. A demonstração formal pode ser usada para fundamentar a verificação.
Resposta correta: A) Uma tripla que expressa a pré-condição, o código e a pós-condição.
Justificativa: a tripla de Hoare é da forma {P} C {Q}, indicando que, se P é verdadeira antes de C, então Q é verdadeira após C.
Resposta correta: A) Predicados que descrevem condições esperadas em pontos do código (pré, intra e pós).
Observação: assertions são usados para especificar o que deve ser verdadeiro em pontos específicos do código durante a verificação.
Resposta correta: A) R é igual a U[X := E] (R é U com X substituído por E).
Justificativa: Pela axiomática de atribuição de Hoare, {Q[X := E]} X := E {Q} descreve a relação entre a pré-condição e a pós-condição após a atribuição.
Olá, alunas e alunos do curso de Fundamentos Matemáticos para a Computação.
Nesta videoólogo, eu vou falar da demonstração de correção.
Para isso, nós vamos verificar, nós vamos iniciar falando da verificação e validação de um programa.
E, no nosso caso, nós vamos estar preocupado com a parte de verificação.
Então, para isso, nós vamos estabelecer o conceito de acertões e entender o uso do acción, de atribuição e de regra condicional para demonstrar a correção de um programa.
Bom, para a verificação, ela visa garantir a correção do programa.
Isso significa que o programa segue a gente quer ter certeza que ele segue suas especificações.
Isso não significa que o programa vai resolver o problema, proposto pelo cliente.
A validação do programa, sim, garantir que o programa atende as necessidades originais do cliente.
E isso nós não vamos discutir aqui nesta aula.
Bom, então, a verificação de um programa ela ocorre via testes ou via demonstração de correção.
No caso dos testes, a gente vai ter algum conjunto de dados representativos para entrada desse programa e vamos esperar que a partir dessas entradas representativas as respostas estejam de acordo com o esperado.
Na demonstração de correção, nós já vamos utilizar o que temos aprendido aqui em ter a luz de lógica.
Nós vamos utilizar técnicas, nós vamos aplicar um sistema de lógica formal para poder verificar a correção daquele programa.
Então, na verdade, os testes, eles são muito aplicados para a gente agoliar o funcionamento de um programa, se ele está correto.
Em geral, a demonstração você vai se aterar ela para trechos mais específicos, para apontos mais específicos do código que você quer fazer um análise, mas que você entra ali naqueles aspectos.
De uma maneira mais abrangente, você pega realmente um conjunto de dados representativos e testa o seu programa.
Bom, para isso, então, para entender como a gente pode estar fazendo essa demonstração entre esses trechos mais interesse do programa que queremos a ferir a sua correção deles, nós podemos considerar o conceito de assertões.
Para isso, foi um pessoal seguinte, nós temos, seja x, uma coleção arbitrária de valores de entrada.
O íbito, a você dos valores de saída, que vão depender de x à medida que ele sofre que essas entradas, ela sofre a a ação das instituições constantes no programa.
Bom, nós vamos ter que x como condições que os valores de entrada são supostos de satisfazer, ou seja, nós temos aqui um predicado que esses valores de entrada devem satisfazer.
Além disso, nós vamos ter aqui um outro predicado binário que vai descrever condições que os valores de saída devem satisfazer.
Considerando, neste caso, os valores de entrada fornecidos.
Bom, dessa forma, vamos tentar ilustrar com um exemplo.
Suponhe que x pertença ao domínio de valor numérico e que a precondição para isso, a condição que essa entrada deve satisfazer, é ser positiva.
Bom, então, nós vamos ter um valor numérico de saída obtido pelas estupações.
Estruções executadas pelo programa onde, essas, essa manipulação, ela vai levar a uma relação do títio y² igual a x, ou seja, para todo o valor de entrada que atendas condições, então nós vamos ter essa relação verificada.
Dessa forma, reescrevendo com o contexto que apresentado, nós teríamos que para todo x para x maior que zero, nós vamos ter que as alterações títas pelo programa que vão nos fornecer esse valor y elevado ao quadrado, você igual a x.
Então, os valores de saída devem satisfazer a esse predicado binário.
Bom, para representar isso de uma maneira mais clara na verificação da correção, nós vamos fazer uso da tripla de holl.
Nesse caso, nós vamos ter uma precondição, o programa e uma post-condição, onde o quantificador universal que está presente aqui, ele fica subintendido.
Bom, nesse caso, as acerções, elas vão ser vistas como predicados que afirmam o que é supposed de servir a da deiro sobre as variáveis do programa em cada ponto do código.
Então, essas acerções, elas indicam a nesse ponto que a gente tem essa precondição, depois nós vamos ter nesse ponto, espera-se que a gente tenha atingido o comportamento do código satisfaza esse tipo de condição, depois esse tipo de condição, assim sucessivamente até o final.
Então, uma maneira de você verificar isso é olhar como essas acerções ocorreram, foram satisfeitas, de trás para frente, e a gente vai abordar isso já já.
O termo S, N, C, ele é uma posição individuais em que o seguimento de programa é dividido, ou seja, são os trechos do programa que modificam os valores de entrada provocando uma saída que se espera ter determinado comportamento pelas acerções estabelecidas.
Bom, nessa forma, o programa é inversal de todo correto, se cada condicional através dessa tripla de Henry, ela é satisfeita.
Bom, assim chegamos ao acionamento de atribuição.
Seja uma proposição declarada na forma X igual a E, onde S e E é uma expressão.
A correção dessa proposição vai ser demonstrada por uma tripla de Henry, onde as acerções R e R e mais U tem que estar relacionadas de uma forma especial.
Ou seja, nós vamos ver esse relacionamento em sequência de que maneira.
Então, de forma resumida representando o acion, nós vamos ter a tripla, nós vamos ter o trecho de código, vamos identificar o trecho de código que vai modificar, seguindo aqui nesse contexto, o acionamento de atribuição, uma relação de atribuição, e vamos verificar a pré-aposquondição de que maneira.
Suponha que nós tenhamos essa precondição, essa atribuição, e espera ser essa posquondição.
Então, nesse contexto, nós temos essa acerção, essa primeira acerção que é a pré-aposquondição, essa segunda acerção, e nós temos aqui a proposição, ou seja, a parte em que o programa atua em cima dos valores.
Bom, o que nós podemos fazer? Como que nós podemos verificar esse progresso? Nós começamos aqui pela posquondição, avaliando que X tem que ser maior que zero, mas para X ser maior que zero, a atribuição aqui, ela vai implicar que X menos 1 seja maior que zero, o que vai me levar a X maior que 1, o que vai satisfazer a minha pré-aposquondição? Bom, eu confesso que você olhando assim, né, a coisa parece meio óbvia, vamos trabalhar mais essa ideia, como deveria ser a pré-apondição, por exemplo, quando a gente tem um trecho de código, como esse que eu estou listando aqui? Bom, nesse contexto, novamente nós vamos analisar a posquondição, então é esperado que X seja igual a Y.
Bom, para isso, o que eu faço? Eu volto aqui, então, na minha proposição, no meu trecho que modificou aqui os valores, que o meu trecho de código, e aí eu verifico que sendo X igual a Y, isso significa que eu vou ter Y igual a X menos 2.
Isso significa que a minha pré-apondição, ela vai ter que satisfazer de alguma forma.
Y, ela vai ter que satisfazer Y igual a X menos 2, ou X menos Y menos 2 igual a 0, ou X igual a Y menos 2.
Qualquer forma que você reescreva isso? Por que? Porque dada essa posquondição, esse termo é quando se eu olheço o código de trás para frente.
Dada essa, se eu estou esperando que essa posquondição ocorra, isso significa que esse termo aqui tem que valer Y.
Então, na minha pré-apondição, o Y tem que se relacionar com o X por esta relação.
Mais um exemplo, vamos verificar a correção desse trecho de código, onde eu tenho essa entrada e espero essa saída.
Como vou fazer isso? Novamente vamos usar essa estratégia de avançar do fim para o início de que forma.
Então, é esperado como uma posquondição que eu faço a inversão dos valores de entrada.
Vamos checar o efeito sobre a novamente de trás para frente, o efeito que gerou essa posquondição a partir da alteração feita pelo código.
Então, nesse caso, o que isso significa? Isso significa que eu vou ter um ípolo recebendo o tempo.
Mais um ípolo aqui vale a, isso significa que tempe, vale a lear.
Repare que eu apenas repeti o X igual a B, porque ele não foi manipulado por essa instrução.
Ele vai ser manipulado aqui.
Chegando nesse ponto, então, verificando essa precondição para essa instrução, agora vou avaliar essa precondição com uma posquondição para essa instrução e verificar o impacto dessa instrução.
Novamente, voltando no meu código, o que eu vou ter nesse caso? Aqui, eu mexi no X, então, o meu tempo, ele permanece aqui, e o que vai acontecer é o que? Como o X valia B, na posquondição aqui, nesse contexto, eu vou ter Y valendo B.
Agora, novamente, esse termo que é a minha precondição para essa instrução, se torna a minha posquondição para essa instrução, e eu vou avaliar o efeito dessa instrução aqui.
Então, novamente, o que vai acontecer é que eu mexo com tempo X, então, isso significa o que? Não vou mexer com o I, mas o meu tempo, ele está passando o valor A para X.
E isso indica o que? Que é a inversão de fato reú? Então, o programa está funcionando, conspirado.
Bom, mais uma exemplo.
Então, nesse caso, o que suponha que eu tenha essa precondição X igual a 3, essa posquondição X igual a 7, avançando do fim, para o início o que nós vamos ter? Então, eu tenho uma entrada a 3, uma saída a 7, o que vai acontecer? Eu pegando e atribuindo.
Se meu z tem que valer 7, isso significa que o meu X mais I, então, vai estar valendo 7.
Na minha próxima instrução, eu atribuo um valor para I, pessoal.
Então, para eu ter essa posquondição aqui, a minha precondição vai ser X mais 4, igual a 7, onde o I, pessoal aqui, está sendo substituído pelo valor 4.
Dessa forma, se eu fiz essa conta aqui, eu chego exatamente na minha precondição X igual a 3.
Certo? Passando 4 para o outro lado.
Bom, uma outra forma da gente verificar é a através de quando nós temos que lidar com uma reira condicional.
Então, por exemplo, aqui nós temos duas possibilidades de seguir as instruções do código.
Se a condição B ocorre, e se a condição B não ocorre.
Então, para isso, eu vou verificar a minha precondição e vou verificar a condição B para executar o trecho de código, a proposição estabelecida pelo código, e verificar a posquondição.
Ou, que se li esse senão aqui, eu tenho a minha precondição, a minha condição B não é verificada, nesse caso, eu executo a instrução nessa parte, nesse P2 aqui, nesse trecho P2 do código, e verifico se, pela minha acertão, é, se eu estou com a posquondição desejada.
Então, nesse caso, eu tenho, como resultado, uma tripla de sempre a execução de uma tripla de Rory.
Seja pela ocorrência dessa condição ou não.
Bom, então, demonstrar a condição de cada ramificação da declaração condicional é o que vamos precisar fazer.
Com, nesse caso, aqui, eu tenho que verificar, então, primeiro passo, identificar as triplas envolvidas.
Eu tenho aqui a situação em que, dada a minha precondição, a minha condição B ela é essa desfeita, aí, eu vou avaliar a execução do código, certo? E verificar se a minha posquondição foi obedecida.
No outro caso, se B não acontecer, eu vou manter a minha precondição, verificar a não ocorrência de B, que é a negação disso aqui, executar o trecho de código correspondente, e verificar se a minha posquondição, que é a mesma, pros dois casos, se verifica.
Bom, então, vamos ver isso.
Iniciando aqui, pelo primeiro condição, nós já observamos que ela não ocorre, ela é falsa, porque, dado que n igual a 5, a minha condição avalia, se n for maior ou igual a 10, para executar essa instituição, então isso não vai acontecer.
Vamos para o próximo trecho.
No próximo trecho, nós temos mantido a precondição, verificarmos agora que o N da precondição satisfaz o fato de ser menor que 10, porque não se te fez isso aqui, o que vai acontecer nesse caso? Vou executar esse trecho de código, que é somar a N, sim, o que me leva a I, isso é igual a 6.
Então, olhando agora essa tripla e aplicando o accioma de atribuição, vamos analisar o seguinte para esse trecho de código.
Dado meu I, um igual a 6, que é a minha posquondição esperada, voltando às equidades para frente, nós verificamos que a minha precondição se torna N mais 1, igual a 6.
O que significa o N mais 1, igual a 6, N igual a 5, que é a minha precondição.
Então, está o que? Está correto.
Ou, por exemplo, nós temos agora nesse trecho de código, que X igual a 4, como a precondição e como a posquondição, X igual a 3.
Então, isso significa que nesse ponto aqui, X vai estar valendo 4.
E nessa saída aqui, o I, que está valendo 3.
O que vai acontecer? Quando eu verifico, vamos identificar agora de uma maneira mais direta atribla de Rho, nesse caso, o que nós temos? O que valendo X igual a 4, o meu P, X, N, 5, essa condição é essa desfeita.
A minha instrução é Y, X, N, e a posquondição, Y, E, igual a 3.
Por outro caso, eu teria a precondição X, A, 4, a condição, X, A é a maior a igual a 5, o trecho de código, Y é igual a 7, e a posquondição, Y é igual a 3.
Bom, nesse caso, a primeira tripla é a que se mostra na verdadeira.
E quando eu vou, então, usar a prisão à acessão de atribuição, para verificar a correção dela o que eu faço, eu parto de I, o N é igual a 3.
Nesse caso, X menos 1 vai valer 3, eu tenho X igual a 4, a que é a minha precondição.
No segundo caso, ele vai ser falso, então eu não vou ter o que verificar, dada a precondição estabelecido.
Bom, dessa forma, eu acredito que nós vimos já que uma relação bem interessante entre como você pode utilizar a lógica para estar verificando a correção de código, e assim, nós ensinramos o primeiro capítulo do livro.
Eu espero que vocês façam uma boa leitura da sessão 1.
6, que é de onde eu retirei os exemplos e os conceitos aqui apresentados.
Obrigado e até a próxima aula.