[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

Weakest Preconditions

• Pre-post form: {P} statement {Q}

• A weakest precondition is the least restrictive precondition that will guarantee the postcondition

• An example:

      a := b + 1  {a > 1}
  

• One possible precondition: {b > 10}

• Weakest precondition: {b > 0 }