Predicate transformer semantics: Difference between revisions

Revision as of 11:59, 29 November 2022

Revision as of 18:32, 29 November 2022

Line 9:

=== Conventions ===

We use '' T '' to denote the predicate that is everywhere true and '' F '' to denote the one that is everywhere false. We shouldn't at least conceptually confuse ourselves with a Boolean expression defined by some language syntax, which might also contain true and false as BooleansBoolean scalars. For such scalars we need to do a type coercion such that we have T = predicate(true) and F = predicate(false). Such a promotion is carried out often casually, so people tend to take T as true and F as false.

=== Skip ===