Simplified Forward Assignment (Hoare Calculus)

hoare-calculus

Definition

Simplified Forward Assignment

Under specific side conditions, the assignment rule can be simplified to:

Side Conditions:

1. does not occur in .
2. does not occur in .

Intuition

This rule is a special case of Floyd’s rule. When the variable is not present in the precondition or the expression , the “old” value of does not influence the validity of , and the facts in remain unchanged by the assignment.

Derivation from Floyd’s Rule

Applying the full Floyd’s rule with the side conditions:

• (since )
• (since )

The postcondition becomes . Since no longer appears in the formula, the quantifier can be dropped, yielding .

Restricted Use

This rule is invalid if the side conditions are not met. For example, is correct, but results in a contradiction ().