这个是比较针对期末复习的知识点整理，根据我的复习随缘更新，如果发现有些部分没写那就是因为我还没复习到（大概）
（PS：这些知识点中有很大部分来自老师的PPT，也有一部分来源于学长学姐整理的资料，最后也有一小部分来源于我自己的总结）
一.简答题
1.串行系统的程序正确性定义。
2.有限状态机的不足之处。
3.Moore机的六元组定义
4.Mealy机的六元组定义
记忆方法：Mealy机与Moore机的不同在于λ不同，所以在记忆的时候只需要记住一个，然后再分别记忆λ即可。
5.Statecharts中状态节点的类型。
6.Petri网模型上迁移间的关系
7.几种特殊Petri网对各类关系的描述能力。
8.Petri网的行为性质（能列出三种并解释含义）
二.分析证明题
1.Floyd 前后断言法（例5.3.1、例 5.3.2、课后5.7）
（1）归纳断言法 ---- 证明部分正确性
（2）良序集法 ---- 证明终止性
2.Hoare 公理化方法，证明程序部分正确性（例5.3.3、课后5.8(1)）
3.Dijstra最弱前置谓词法，证明程序完全正确性（P133下数组求和题、课后5.9）
4.有限状态机：
（1）给出定义形式的一个有限状态机，画出其状态转移图、状态转移表、状态转移矩阵；或给出状态转移图形式的有限状态机，写出其定义形式。
（2）写出有限状态机所接受的语言集合。
5.Petri网：（课后3.1、3.7、3.8）
（1）化简。
（2）覆盖树生成。
（3）有界性、活性、可逆性分析。（可结合化简或覆盖树）
三.应用题
1.有限状态机（课后2.6、课后2.8）、Moore机（图2.4、课后2.4(1)）、Mealy机（图2.5、课后2.4(2)）设计。
2.有限状态机复合。(生产者-消费者系统、模三模四同步、异步复合)
3.Statecharts设计电梯控制系统。
4.Petri网设计。（哲学家、例题生产线、课后生产线、生产者-消费者、消防）