Spojenie programov 3

• Podmienené vlastnosti: (mnoziny H, Z: obidve sú mnozinou nepodmienených vlastností)

hypotéza / záver

• Podmienená vlastnost programu F: hypotéza aj záver môzu byt vlastnostami programu F, G, F ? G pre nejaký generický program G

• význam: vezmeme hypotézu ako predpoklad, záver sa dá dokázat z „textu“ F

• Príklad:

• Program F

  declare x: int
  
  assign [ y := ?y if x ? 0 ? y > 0 ] ? x := x ? 1

end{F}

• nech x sa nemení mimo F (y sa môze menit aj mimo F)

• príklad podmienenej vlastnosti:

  • Hypotéza: y ? 0 is stable in F ? G
  • Záver: y > 0 ? y < 0 in F ? G

Previous slide

Next slide

Back to first slide

View graphic version