weakest precondition

In the context of program logics, a weakest precondition for a given command and postcondition is a predicate (on program states) such that, for any predicate , if and only if .