&gt; It&#x27;s a guess, but I think GP uses &quot;operational&quot; as a synonym for &quot;imperative&quot;.<p>Not really. It&#x27;s also possible to reason non-operationally about imperative programs, e.g., using predicate transformer semantics. It&#x27;s also possible to reason operationally about non-imperative programs.