Dokazovanie tvrdení o priradovacích príkazoch

• {p} x := E {q}

1. Nahradíme x v q za E (oznacenie qxE)

2. Ukázeme, ze p T qxE

• ak E = e0 if b0 ~ ... ~ en if bn tak výraz qxE bude takýto: (b0 ? qxe0) ? ... ? (bn ? qxen)) ? ((?b0 ? ... ? ?bn) ? q)

• môze sa písat aj v tvare

  {p ? b0} x := e0 {q}
  
  …
  {p ? bn} x := en {q}
  {p ? (?b0 ? ... ? ?bn) ? q}

• Poznámka.

  • Znak ? budeme pouzívat ako oznacenie logickej implikácie.
  • Znak ? oznacuje jednak logickú ekvivalenciu, jednak syntaktickú ekvivalenciu. Význam je zrejmý z kontextu.

Previous slide

Next slide

Back to first slide

View graphic version