New answers tagged software-verification
2
The book that defines TLA+ is "Specifying systems" by Leslie Lamport. TLA+ is a language for writing mathematics (TLA+ is based on Zermelo-Fraenkel set theory).
TLA+ includes temporal formulas, which can describe hardware and software systems. PlusCal is an algorithm language (user manual) that is translated to TLA+. So systems can be described ...
1
This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops.
Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda calculus (with or without types: types don't affect evaluation), you want a quantity (a positive integer) that decreases at each reduction step.
Such a quantity ...
answered Mar 31 at 22:39
Gilles 'SO- stop being evil'
40.1k7 gold badges108 silver badges171 bronze badges
Top 50 recent answers are included
