References:
Imperative language
Statement: declaration of fact or claim. e.g. “Semantics is easy.”
声明/断言：对一个事实或者断言的声明。比如，“语义学是简单的”。
Command：order to do something. e.g. “Study the book until you have understood it.”
命令：指示去做某一件事。比如，“好好学习这本书，一直学到懂为止。”
Expressions are evaluated, Commands are executed.
Big step semantics: $(c,s) \Rightarrow t$. Command $c$ started in state $s$, terminates in state $t$.
use $\Rightarrow$:
$(Skip, s) \Rightarrow s$
$(x ::= a, s)$ $\Rightarrow$ $ s(x:= aval\ a \ s)$
$\frac{(c_1,s_1)\Rightarrow s_2 \ \ (c_2,s_2)\Rightarrow s_3}{(c_1;;c_2, s_1) \Rightarrow s_3}$
Inverted Rules:
$\frac{(c_1;;c_2, s_1) \Rightarrow s_3}{\exists s_2. (c_1,s_1)\Rightarrow s_2 \ \wedge \ (c_2,s_2)\Rightarrow s_3}$
Big step rules:
use $\rightarrow$:
(commands, state) $\rightarrow$ (commands, state)
or
$(c,s) \rightarrow (c’, s’)$
==> “fist step in the execution of c in state s leaves a “remainder” command c' to be executed in state s'“
A pair (c,s) is called a configuration.
If $cs \rightarrow cs’$ we say that cs reduces to cs'.
A configuration is final iff $\nexists$ $cs’. \ cs \rightarrow cs’$
$(SKIP, s)$ is final since $SKIP$ is the empty program. Nothing more to be done.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?