记录一下《Formal Methods》第二章的学习心得
本章节主要介绍了GC语言，分：语法、语义、程序图、可替代部分以及扩展的控制结构这几个方面。
第一部分语法，主要讲了两个比较重要的语法点，赋值符号（：=）和跳过符号（skip），其中赋值符号的作用是对变量进行赋值，skip结合后边对边（edge）的定义，指得是从一条边的起点跳到终点。命令可以是三种不同的组成方式，按照写定的顺序执行和在条件语句处进行判定以及循环。书中C和GC主要定义了操作和条件的集合。根据语法可以做出相应的语法树，同时语法树不需要括号就可以表示语句的执行顺序。
第二部分展开介绍了程序图，首先引入了边edge的概念，表示对程序图的一种限制，同时给出了起始节点和终止节点的定义。二者和语句中的内容共同组成了程序的边集。
如果我们要在两个被执行的语句中进行选择，那我们就使用相同的源节点和目标节点，复杂一些的类似运用到do语句的时候需要使用循环，运用到循环结构时，我们将源节点和目标节点作为一个节点。（对于曲边的理解是，不确定是否要执行动作，如果满足判定条件则执行）
第三部分介绍了GC语言的语义，其中需要定义一个语义域来反应变量值的范围，同时还需要定义语义函数来表达语句动作的含义。在定义布尔表达式时运用了两个变量A、B。A本身或者组合形成算数表达式，结果为具体数值，B本身或者组合形成布尔表达式，结果为布尔值。
补充：&&和&的区别在于，&&第一个条件不成立自动退出，若成立再继续检查后续的条件；&则检查所有条件看是否同时成立。
后边对于边的定义增加了一部分，动作可以放在初始节点和终止节点中间，并且和边结合来共同定义语句。同时也可以指代数组，数组下标同样适用边定义来表示，两个组合起来即可表示数组。
第四部分介绍GC语言的语句中可替代的部分。重点介绍了三种结构，第一种deterministic version，其中引入了一个参数d，用来代表判断结果，每做一次判断就将判断结果存储到d中，并以此重新组成边定义的语句，这样写能够避免语义函数的定义域与其他语义函数的定义域相交，产生不必要的歧义。
第二种evolving version中直接更为详细的罗列出了除了b1和b2之后的其他情况，这样就使得程序的判定条件能够完全覆盖所有情况。
第五部分介绍了几种其他的控制结构，首先介绍了两种循环控制命令，break和continue，其中break指的是循环执行到Break语句时终止并退出循环，继续循环之后的动作。continue语句则是继续到循环开始的地方执行。在构造边的时候为了表示出来这两个控制命令，需要额外加入两个节点来更好的表示遇到控制命令后程序的执行顺序，这两个控制命令主要应用在do循环当中，其它循环不需要使用。
后边介绍了一个嵌套在do循环外的try catch结构，其中进入结构之后，do循环完成动作后经过throw命令返回出一个值，根据返回值比对catch中的值从而执行catch中对应的动作。在构造边定义的时候需要加入γ来指代一个名词表，表中包含catch所对应的名词，当throw返回值对应之后继续进行catch中的动作。其中最为复杂的E’和γ’指的是加入try catch语句之后的动作和条件环境，γ’是指γ逐渐生成的一个过程，可以将γ'理解为生成γ过程的中间变量，当程序运行到catch语句之后开始检索catch后对应的名词，并将其输入γ’中，逐渐生成完整的γ即名词表，后边在执行throw e时已有完整的γ表，因此可以进行对应，从而执行完整的程序。