Fundamentos Matemáticos para Computação - Demonstração de Correção (Libras)

[Música] Olá alunos e alunos do curso de fundamentos matemáticos para computação nesta vídeo aula 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 asserções e entender o uso do axioma de atribuição e de regra condicional para provar para demonstrar a correção de um programa bom 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 pelo cliente a validação do programa sim garante 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 representativos as respostas estejam de acordo com o esperado na demonstração de

correção Nós já vamos estilizar o que o que temos aprendido aqui em termos 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 avaliar 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 pontos mais específicos do código que você quer fazer uma análise mas concentrada ali naqueles aspectos né 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 que a gente pode estar fazendo essa demonstrações para esses trechos mais de mais interesse do programa que queremos aferir a sua a correção deles nós podemos então considerar o conceito de asserções para isso foi uma pessoa seguinte nós temos seja x uma coleção arbitrária de valores de entrada tá é o y vão ser os valores de saída que vão depender de X a medida que ele sofre que essas entradas né Elas sofrem a ação das instruções constantes no programa bom nós vamos

ter que x como condições que os valores de entrada são supostas 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 nesse caso né os valores de entrada fornecidos dessa forma Vamos tentar ilustrar com exemplo Suponha que x pertença a um domínio de valor numérico e que a precondição para isso a condição que essa entrada deve satisfazer é ser positivo bom então nós vamos ter um valor numérico de saída

obtido pelas instruções executadas pelo programa onde essas essa manipulação ela vai ela vai levar a uma relação do tipo Y ao quadrado igual a x ou seja para todo o valor de entrada que atenda as condições Então nós vamos ter essa relação verificada dessa forma reescrevendo com o contexto aqui apresentado nós teríamos que para todo X para x maior que zero nós vamos ter que as alterações feitas 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 s a esse predicado

binário para representar isso de uma maneira mais clara na verificação da correção nós vamos fazer uso da tripla de Harley nesse caso nós vamos ter uma precondição ou programa e uma pós condição onde o quantificador Universal que está presente aqui ele fica subentendido bom nesse caso as asserções elas vão ser vistas como predicados que afirmam o que suposto ser verdadeiro sobre as variáveis do programa em cada ponto do código Então essas asserções elas indicam a nesse ponto a gente tem essa pré-condição depois nós vamos ter nesse ponto espera-se que a gente tenha atingido o comportamento

do código satisfaça 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 exceções ocorreram foram satisfeitas de trás para frente e a gente vai abordar isso já já o termo S í em si ele é uma opção proposições individuais em que o segmento 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 exceções estabelecidas bom dessa forma o programa ele vai ser dito correto se

cada condicional através dessa tripla de Harry ela é satisfeita bom é assim chegamos ao axioma de atribuição seja uma proposição declarada na forma x = e onde se e ele é uma expressão a correção dessa proposição ela vai ser demonstrada por uma tripante tripla de Harry onde as sessões tem que estar relacionada de uma forma especial ou seja nós vamos ver esse relacionamento em sequência de que maneira né então de forma resumida representando o axioma 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 do que se chama de atribuição uma relação de atribuição né E vamos verificar a pré e após condição de que maneira Suponha que nós tenhamos essa precondição essa atribuição e espera-se essa pós condição Então nesse contexto nós temos essa asserção essa primeira sessão que a pré-condição essa segunda sessão e nós temos aqui a proposição Ou seja a parte 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 pós condição avaliando que X tem que ser maior que

zero mas para XC é maior que zero a atribuição aqui ela vai implicar que x -1 seja maior que zero o que vai me levar a x maior que 1 o que vai satisfazer a minha pré-condição eu confesso que você olhando assim né a coisa parece meio óbvia nós vamos trabalhar mais essa ideia tá deveria ser a pré-condição Por exemplo quando a gente tem um trecho de código como esse que eu tô listando aqui bom nesse contexto novamente nós vamos analisar após condição então é esperado que x seja igual a y 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 trecho de código E aí eu verifico que sendo X = Y Isso significa que eu vou ter Y igual a x - 2 Isso significa que a minha pré-condição ela vai ter que satisfazer de alguma forma Y ela vai ter que satisfazer y = x - 2 ou x - y - 2 = 0 ou x = y + 2 qualquer forma que você Reescreva isso porque porque dada essa pós condição esse termo é quando você olhasse

o código de trás para frente dada essa essa se eu tô esperando que essa pós condição corra Isso significa que esse termo aqui tem que valer Y então na minha pré-condiçã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 Então como é que eu 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 pós condição O que eu faça a inversão

dos valores de entrada beleza vamos checar o efeito sobre a novamente de trás para frente o efeito que gerou essa pós condição a partir da alteração feita pelo código Então nesse caso que isso significa isso significa que eu vou ter um Y recebendo tempo mas o meu Y aqui variar Isso significa que tem que vai valer repare que eu apenas repetir o x igual a B aqui 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 Eu agora vou avaliar essa condição como

uma pós condição para essa instrução e verificar o impacto dessa instrução novamente voltando no meu código o que que eu vou ter nesse caso aqui eu mexi no X então o meu tempo a ele permanece aqui e o que vai acontecer o que que Como o meu x valia B na pós condição aqui nesse contexto eu vou ter Y valendo B agora novamente esse termo que é a minha pré-condição para essa instrução se torna me após condição né para essa instrução e eu vou avaliar o efeito dessa instrução aqui então novamente o que vai acontecer

aqui eu mexo com o tempo e x então isso significa o quê não vou mexer com Y B mas o meu tempo ele tá passando valor Ah para x e isso indica o quê que é inversão de fato eu tá então o programa está funcionando como esperado bom mais um exemplo Então nesse caso aqui Suponha que eu tenha essa pré-condição x = 3 e essa pode condição x = 7 avançando do fim para o início que que nós vamos ter Então eu tenho uma entrada três uma saída 7 o que que vai acontecer eu pegando

e atribuindo se meus item que valer 7 Isso significa que o meu x + y vai vai tá valendo 7 na minha próxima instrução eu atribuo um valor para Y então para eu ter essa pós condição aqui a minha pré-condição vai ser x + 4 = 7 onde o y aqui tá sendo substituído pelo valor quatro dessa forma se eu fizesse a conta aqui eu chego exatamente na minha pré-condição x = 3 certo passando quatro para o outro lado bom uma outra forma da gente verificar é através é quando nós temos que lidar com uma

regra condicional então por exemplo aqui nós temos duas possibilidades de seguir as instruções do código se a condição de ocorre isso a condição b não ocorre então para isso eu vou ver eu vou ter a minha pré-condição e vou verificar a condição B para executar o trecho de código a proposição estabelecida pelo código e verificar após condição ou que seria esse senão aqui eu tenho a minha pré-condição a minha condição b não é verificada nesse caso executo a instrução nessa parte nesse P2 aqui nesse trecho P2 do código e verifico se pela minha sessão é

e se eu estou com após condição desejada Então nesse caso eu tenho como resultado a matrícula de sempre a execução de uma tripa de seja pela ocorrência dessa condição ou não bom então demonstrar a correçã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 pré-condição [Música] a minha condição de ela é satisfeita aí eu vou avaliar a execução do código certo e verificar se a minha pós condição

foi obedecida no outro caso se b não acontecer eu vou manter a minha pré-condiçã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 pós condição que é a mesma para os dois casos se verifica bom então vamos ver isso iniciando aqui pelo primeiro pela primeira condição nós já observamos que ela não ocorre ela é falsa porque dado que n = 5 a minha condição avalia se n for maior ou igual a 10 para executar essa instrução então isso não vai acontecer Vamos para

o próximo trecho no próximo trecho nós temos mantida a pré-condição verificamos agora que o m da pré-condição satisfaz o fato de ser menor que 10 né porque não se desfez isso aqui o que vai acontecer nesse caso vou executar esse trecho de código que é somar a n 5 o que me leva a y = 6 então olhando agora essa tripla e aplicando o axioma de atribuição nós vamos analisar o seguinte para esse trecho de código dado o meu Y igual a 6 que a pós condição esperada voltando a executar de trás para frente nós

verificamos que a minha pré-condição se torna n + 1 = 6 O que que significa o n + 1 = 6 n = 5 que é a minha precondição então tá ok está correto outro exemplo nós temos agora é nesse trecho de código aqui x = 4 como pré-condição e como pós condição Y = 3 então isso significa que nesse ponto aqui o x vai estar valendo 4 e nessa saída aqui o Y tem que estar valendo 3 o que que vai acontecer quando eu verifico vamos identificar agora de uma maneira mais direta a tripla

de Hornet nesse caso o que que nós temos o que valendo x = 4 o meu b x menor que 5 essa condição ela é satisfeita a minha instrução é y = x - 1 e após condição Y = 3 para o outro caso eu teria pré-condição x = 4 a condição x maior = 5 trecho de código y = 7 e após condição Y = 3 bom nesse caso a primeira tripla é a que se mostra verdadeira e quando eu vou então aplicar um axioma de atribuição para verificar a correção dela o que eu

faço eu parto de Y = 3 nesse caso x -1 vai valer três eu tenho x igual a 4 que é a minha pre condição no segundo caso ele vai ser falso então eu não vou ter o que verificar dada a pré-condição estabelecida bom dessa forma eu acredito que nós vimos aqui uma relação bem interessante entre como você pode utilizar a lógica para estar verificando a correção de código tá E assim nós encerramos 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 dos

exemplos e os conceitos aqui apresentados obrigado e até a próxima aula [Música]