On the Definition of Non-deterministic Mechanisms

TL;DR

This paper introduces three equivalent mathematical definitions of non-deterministic mechanisms, providing a clearer and more accessible way to understand and teach the concept, with implications for formal methods like Dijkstra's wp-formalism.

Contribution

It presents three new approaches to defining non-deterministic mechanisms and proves their equivalence, offering a simplified perspective for formal methods.

Findings

All three definitions are mathematically equivalent.

The new approaches facilitate easier understanding and teaching.

Implications for the wp-formalism of Dijkstra.

Abstract

We present here three different approaches to the problem of modeling mathematically the concept of a non-deterministic mechanism. Each of these three approaches leads to a mathematical definition. We then show that all the three mathematical concepts are equivalent to one another. This insight gives us the option of approaching the wp-formalism of Dijkstra from a different viewpoint that is easier to understand and to teach.