用数学去思考.
TLA+
数学描述 vs 编程的方式描述. We witnessed first hand the brain washing done by years of C programming.
概念
抽象：Simplifying by removing details is called abstraction.
我们想system能work right。 work right 意味着满足某些properties。
TLA+能检查的properties是 conditions on individual executions。 不能检查一些概率的，如99% of executions produce the right answer。 Not a condition on a single execution.
TLA+下的基本抽象：
- An execution of a system is represented as a sequence of discrete steps.
Digital system： We can abstract its continuous evolution as a sequence of discrete events. 比如把物理的钟表抽象为按tick运转的。
TLA+ describes a step as a state change.
An execution is represented as a sequence of states.
我们叫a sequence of states为a behavior。
一个system有好多个可能的execution(即behavior).
Science models systems by a state changing with time, usually continuously. We model digital systems by a state changing in discrete steps.
- TLA+ describes a state as an assingment of values to variables.
state machines
描述state machine:
- What the variables are
- Possible inital values of variables.
- A relation between their values in the current state and their possible values in the next state.
Math VS program
Math的表达性更强。如：
- Math可以描述不确定性(someNumber)，
- Math可以用variable描述所有。program要通过很多方式来描述(control state, heap, stack)
- Math更关注于算法
- formula有很多特性(无序性，可拆解)