Example

Program $F$
   declare $x$: integer
   assign
      $y$ := $-y$, if $x$ $0$ and $y>0$
   [] $x$ := $x-1$
end {$F$}

• Unconditional properties:
  • is stable in $F$.
  • $y=0$ is stable in $F$.
  • $y$ not $0$ is stable in $F$.
• Conditional properties:
  • Hypothesis: $y$ $0$ is stable in $F$ [] $G$.
  • Conclusion: $y>0$ $|->$ in $F$ [] $G$
• $G$ shares only $y$ with $F$.