Pular para o conteúdo principal

Questão de Algoritmos e Estrutura de Dados — Algoritmos — JVL Concursos 2025

Algoritmos e Estrutura de DadosAlgoritmos
Código
qg572228
Banca
JVL Concursos
Órgão
Prefeitura de Regeneração - PI
Ano
2025
Nível
Superior
Cargo
Professor de Computação
Assinale a alternativa que descreve, de modo completo, o uso de invariantes de laço para provar correção e terminação de um algoritmo iterativo.
  1. APartir da pós-condição, inverter instruções por leitura textual, aceitar preservação empírica em casos de teste e encerrar o laço quando a guarda permanecer verdadeira.
  2. BEscolher um invariante que vale antes do laço, mostrar preservação a cada iteração, definir uma função variante decrescente em ℕ e concluir a pós-condição a partir de invariante verdadeiro e guarda falsa.
  3. CDerivar o invariante de exemplos executados, assumir que decrementos eventuais bastam para terminar e concluir a prova substituindo a guarda pela pós-condição ao final.
  4. DFixar o invariante igual à pós-condição, provar que ele se torna verdadeiro no meio do laço e finalizar quando o invariante coincidir com a guarda ainda verdadeira.
Revelar gabarito e comentário

GabaritoB — Escolher um invariante que vale antes do laço, mostrar preservação a cada iteração, definir uma função variante decrescente em ℕ e concluir a pós-condição a partir de invariante verdadeiro e guarda falsa.

Comentário gerado por IA. É um apoio ao estudo, ancorado em fontes, mas pode conter imprecisões — confira sempre na fonte oficial (lei, súmula, edital e gabarito da banca). Encontrou um erro? Use “Reportar”.

Invariantes de laço para prova de correção e terminação

Gabarito: letra B. A alternativa descreve corretamente o método: escolher um invariante verdadeiro antes do laço, mostrar que ele se preserva a cada iteração, definir uma função variante estritamente decrescente em ℕ (garantindo terminação) e, ao final, da invariante verdadeira e da guarda falsa deduzir a pós-condição.

Invariantes de laço são condições lógicas que permanecem verdadeiras antes e depois de cada iteração. Para provar correção parcial, mostra-se que o invariante vale na entrada do laço e que é preservado pelas iterações. A terminação é provada com uma função variante que diminui estritamente a cada passo e é limitada inferiormente. Quando o laço termina (guarda falsa), o invariante ainda é verdadeiro e, junto com a negação da guarda, implica a pós-condição.

Alternativa A — ❌ Incorreta

Partir da pós-condição e inverter instruções não é um método formal. Aceitar preservação empírica (testes) não prova correção para todos os casos. O laço termina quando a guarda se torna falsa, não verdadeira.

Alternativa B — ✅ Correta ⟵ GABARITO

Descreve precisamente os três passos: invariante inicial, preservação, função variante decrescente em ℕ, e conclusão da pós-condição. É a definição clássica do método.

Alternativa C — ❌ Incorreta

Derivar invariante de exemplos não é uma prova formal; decrementos eventuais não garantem terminação (a função deve ser monótona decrescente e limitada). Substituir guarda pela pós-condição não faz sentido lógico.

Alternativa D — ❌ Incorreta

O invariante não deve ser igual à pós-condição (geralmente é mais fraco). Provar que o invariante se torna verdadeiro no meio do laço não assegura correção. Finalizar com guarda ainda verdadeira contradiz a terminação.

Gabarito: letra B.

Link permanente: /questoes/qg572228