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/语义

原文地址:https://www.cnblogs.com/teafrogsf/p/Formal_Methods.html