Predicative programming

Predicative programming is a methodology for program specification and refinement. The central idea of predicative programming is that each specification is a predicate (generally written as a boolean expression) that is true of acceptable behaviours and false of unacceptable behaviours. It follows that refinement is reversed implication universally quantified over behaviours:

Commands in a programming language are considered to be a special case of specifications—special only because they are compilable. For example, in an environment where the program variables are ${\displaystyle x}$, ${\displaystyle y}$, and ${\displaystyle z}$, the command ${\displaystyle x:=y+1}$ is considered equivalent to the predicate (represented here by a boolean expression)

...
Wikipedia