Formal Methods: An Appetizer by The Nielsons学习笔记

这本书我可能更倾向于将英文放在主要位置，因为它里面的内容比较前沿，用英文更加合适。

词汇表

vending a. 出售（东西）的
subtle a. 微妙的，不易察觉的
notion n. 观念
teaser n. 难题；先导式广告（也就是说这本书里提到后面的内容会加个teaser的tag，这不比Artin的书人性化？

前言

阳间很多了，但还是不能看懂。

序章

Formal Methods/形式化方法

大概讲了一下Formal Methods的广泛应用，及无论IT system大小，semantics(语义学)在其中的作用让Formal Methods变得很重要。
还推荐了一本文笔更好的描述Formal Methods如何在safety and security of IT systems应用的书：
Kevin Hartnett: Hacker-Proof Code Confirmed. Quanta Magazine, 2016.

Program Graphs/程序图

有些时候我们需要分析软件有没有照其所设计的一样工作。
一个model（模型）是系统的抽象，它将会聚焦在系统的某些部分同时忽略其他部分。需要注意一个model不仅描述了IT system的结构，还有它作为一种合适级别抽象的意义。
program graphs聚焦于用抽象的方式展现一个系统如何从一个点到另一个点的工作。动作的意义通过定义它们的语义形式化，这给了程序图含义更精确的描述。

Guarded Commands/命令保护

Program Verification/程序验证

Program Analysis/程序分析

Languaged-Based Security/语言层面的安全？

Model Checking/模型检测

Procedures/过程

Concurrency/并发

Programming Projects/编程计划

Program Graphs/程序图

这一章将会发展一种基于Program Graphs的对语义的符号观念。

Program Graphs/程序图

一个program graph (PG)由以下部分组成：
(Q)：一个有限点集；
一个initial node（初始结点）(q_S)，一个final node（最终结点）(q_T)
(Act)：一个action（行为）集；action此处又称作assignment。
(Esubseteq Q imes Act imes Q)：一个有限边集。一条边((q_u,alpha,q_v))有一个source node（源点）(q_u)和一个target node（目标点）(q_v)，且它被action (alpha)标记。
此处需要求不能有自环，终点没有出边。用(PG=(Q,q_S,q_T,Act,E))来总结一个程序图。
Program graphs和有限自动机很像，我们可以类比非确定性有限自动机定义从(q_u)到(q_v)的formal language（形式化语言）

[L(q_u ightsquigarrow q_v)(E)={alpha1cdotsalpha n|exists q_0,cdots,q_n:forall iin{0,cdots,n-1}:(q_i,alpha_{i+1},q_{i+1})in E,q_0=q_u,q_n=q_v}. ]

因此可以定义(PG)的language

[L(PG)=L(q_S ightsquigarrow q_T)(E). ]

书中还简单阐述了program graph和flow chart的区别，这里懒得写。

Semantics/语义