程序的语义：程序P表示一个状态的转换，而状态是指一个从变量到值得映射。
大步语义：给定程序c和状态s和t，
$(c,s)\Rightarrow t$
表示程序c可以把状态s转换到状态t。
大步语义-skip语句、赋值语句和顺序的规则
其中$s( v:= [e]_s )$ 的含义为，该状态和s一样，除了v的值变为$[e]_s$之外。
标签：语句,状态,入门,语义,形式,程序,大步 From： https://www.cnblogs.com/zhaoke271828/p/17009570.html
程序的语义：程序P表示一个状态的转换，而状态是指一个从变量到值得映射。
大步语义：给定程序c和状态s和t，
$(c,s)\Rightarrow t$
表示程序c可以把状态s转换到状态t。
大步语义-skip语句、赋值语句和顺序的规则
其中$s( v:= [e]_s )$ 的含义为，该状态和s一样，除了v的值变为$[e]_s$之外。
标签：语句,状态,入门,语义,形式,程序,大步 From： https://www.cnblogs.com/zhaoke271828/p/17009570.html