Create a function which takes an atomic command r and a post-condition q and returns the weakest precondition p that makes the SSIL triple {{p}} r {{q}} valid. This function will be used in the analysis of atomic commands inside blocks, while other structures will be used for the analysis of the regular commands C+C and C*.
Create a function which takes an atomic command
r
and a post-conditionq
and returns the weakest preconditionp
that makes the SSIL triple{{p}} r {{q}}
valid. This function will be used in the analysis of atomic commands inside blocks, while other structures will be used for the analysis of the regular commandsC+C
andC*
.