weakest precondition
stands for weakest precondition of under program S.
It’s stronger than weakest liberal precondition, and guarantees termination.
However, we often refer to wlp when we talk about weakest precondition.
stands for weakest precondition of under program S.
It’s stronger than weakest liberal precondition, and guarantees termination.
However, we often refer to wlp when we talk about weakest precondition.