Is there a validator to verify if an implementation of an algorithm respects the TLA+ specification? Can somebody please tell me (some of) the main differences between TLA+ and JML?
> Is there a validator to verify if an implementation of an algorithm respects the TLA+ specification?
TLA+ has some tools to do this, if you write your implementation in some TLA+-specific language like PlusCal. But this would be the sort of "end-to-end" verification that TLA+ proponents would regard as only being feasible for relatively simple software.
Relatedly, JML basically adds support for "design by contract" specifications to the Java programming language - expressing preconditions, postconditions and invariants. These can be quite useful, but the focus with TLA+ - in this thread and elsewhere - seems to be rather on "deeper" properties that encompass entire systems in a more global and cross-cutting way, and are thus inherently harder to manage with simpler tools.
