Nos últimos vinte anos, houve um progresso lento, porém constante, no uso de especificação formal, no desenvolvimento de software. Nos métodos de especificação formal, o objetivo de se produzir especificações consistentes, completas e corretas é obtido por meio de enunciados matematicamente prováveis. Uma especificação formal pode assim ser checada, em termos de inconsistências e contradições, antes de ser codificada, utilizando-se uma linguagem de programação. A lógica de primeira ordem pode ser uma base para se descrever uma especificação formal. Para isso, são utilizados símbolos matemáticos que expressam um significado importante. Uma lista dos principais símbolos é mostrada abaixo.
| Símbolo | Significado |
|---|---|
| !$ \forall !$ | para todo |
| !$ \exists !$ | existe |
| !$ P \equiv Q !$ | P é logicamente equivalente a Q |
| !$ \sim p !$ | negativa de p (not p) |
| !$ p \wedge q !$ | p e q |
| !$ p \vee q !$ | p ou q |
| !$ p \rightarrow q !$ | se p, então q |
| !$ P \Rightarrow Q !$ | P implica Q |
| !$ p \leftrightarrow q !$ | p se e somente q |
| !$ \ni !$ | tal que |
As sentenças abaixo foram escritas a partir dos símbolos lógicos citados no texto e de símbolos encontrados na Matemática, assumindo x, y e z valores numéricos e p e q valores lógicos.
- !$ \forall x, \, y, \, z !$, !$ x>y \wedge y>z \rightarrow x>z !$
- !$ \exists x \ni x> 10 \vee x+y<100 !$
- !$ \forall x,y \in \mathbb{N} \rightarrow x+y \in \mathbb{N} !$
- !$ \exists x, y \in \{1, \, 2, \, 3, \, 4 \} \ni x+y \in \{ 1, \, 2, \, 3, \, 4 \} !$
- !$ \forall x, y \in \{ 1, \, 2, \, 3, \, 4 \} x>y \rightarrow x - y \in \{1, \, 2, \, 3, \, 4 \} !$
Acerca dessas sentenças e a partir do significado dos símbolos lógicos e matemáticos, julgue o item a seguir.
A instrução de número 3 expressa que a soma de dois números naturais é também um natural.