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.1k77 gold badges108108 silver badges171171 bronze badges
Top 50 recent answers are included
Related Tags
software-verification × 109formal-methods × 29
model-checking × 23
logic × 17
hoare-logic × 15
proof-techniques × 13
correctness-proof × 10
programming-languages × 9
automata × 7
functional-programming × 6
linear-temporal-logic × 6
computation-tree-logic × 6
algorithms × 5
reference-request × 5
semantics × 5
program-correctness × 5
formal-languages × 4
graphs × 3
computability × 3
satisfiability × 3
type-theory × 3
concurrency × 3
first-order-logic × 3
induction × 3
software-engineering × 3