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.