下载文档原格式
淺談形式化方法楊東屏使用電腦的人都會使用某種程序語言,用它來編寫程序。
電腦是不理解程序語言裡各個符號的含意的,但是它可以根據程序裡不同符號的不同排列順序正確地執行編寫程序的人要求做的事情。
這說明不含任何意義的不同符號的排列規律可以表達一定的數學規律。
實際上連唸初中的學生都知道這個事實,例如當他們由式子:−(a+b−c)得到−a−b+c時腦子裡想的是:表達式裡的括弧前面若有負號且當人們要取消括弧時原括弧內每個項前的正負號要改變,把正號變為負號,負號變為正號;而當括弧前面沒有負號時,可以只取消括弧而不對括弧內的符號做任何改動。
這裡想的只是符號排列的變化規則而不直接去想任何數學規則。
同樣地,當他們把x=y−z變為x+z=y時他們也只是考慮符號排列的變化規則:移項時變該項前的正負號。
這種用符號排列的規則去表達一定的數學內容的方法就是一種形式化方法。
本文要著重介紹一下數理邏輯裡研究的有關形式語言的一些結果,希望藉此介紹一些關於形式化方法的知識。
形式化方法是數學長期發展過程中產生的。
古代的埃及人和巴比侖人都知道很多數學知識。
例如古埃及人知道計算正方錐體體積的方法,古巴比侖人知道直角三角形斜邊長度的平方等於二直角邊長的平方和。
但是他們也有些錯誤的結論,例如古埃及人認為其邊長分別是a、b、c、d的四邊形面積公式是(a+b)(b+d)2數學傳播十八卷一期民83年3月人們使用了形式化方法,用無任何直觀內容的抽象的符號表示幾何對象,用關於抽象符號的抽象的關係表示幾何關係,而這些對象和關係只滿足公理裡所陳述的邏輯關係。
在證明過程中只依賴於這種邏輯關係而不依賴於這些符號的直觀含意。
這樣把幾何對象和他們的直觀含意脫離開,防止了錯誤直觀的潛入,從而保證了數學推理的正確。
這樣就開始用形式化的方法去處理數學系統。
Hilbert 建立的歐幾理德幾何系統是這方面的典範。
1879年Frege在他的書Begriffss-chrift裡給出了邏輯系統謂詞演算的形式系統為形式化各種數學系統提供了邏輯框架。
形式化方法在软件工程中的应用研究1. 引言形式化方法是一种基于严格逻辑和数学原理的软件开发方法，通过数学符号和形式语义来描述和验证软件系统的正确性。
在软件工程领域，形式化方法被广泛应用于系统建模、验证和验证等方面。
本文将详细探讨形式化方法在软件工程中的应用，并分析其优缺点。
2. 形式化方法概述形式化方法是一种基于形式语义和数学推理的软件开发方法。
它通过数学描述和推理来确保软件系统的正确性。
形式化方法可以分为两类：形式规约和形式验证。
形式规约是指使用形式语义来描述软件系统的行为和约束条件。
形式验证则是使用数学推理和模型检测等技术来验证系统规约的正确性。
3. 形式化方法的应用场景3.1. 系统建模形式化方法可以用于系统建模，帮助开发人员准确地描述系统的功能和行为。
通过使用形式化规约语言，可以清晰地定义系统的状态和转换条件。
形式化方法还可以准确地描述系统的约束条件，如时序要求、安全性要求等。
这样可以在系统设计的早期发现问题，减少后期调试和维护的工作量。
3.2. 系统验证形式化方法可以用于系统验证，通过形式化规约和数学推理技术，可以对系统的行为和性质进行严格的验证。
形式化验证可以帮助发现系统在设计过程中可能存在的错误和缺陷，并提供修复方案。
形式化验证还可以帮助验证系统的正确性和安全性，确保系统满足设计要求并防止系统漏洞和入侵。
3.3. 代码生成形式化方法还可以用于代码生成，通过形式化规约生成可执行的代码。
由于形式化规约具有严格的语义和约束条件，可以确保生成的代码与规约一致，从而提高代码的正确性和可靠性。
形式化方法还可以生成高性能的代码，通过优化规约和自动化代码生成，可以减少代码的错误和冗余，提高软件系统的性能和效率。
4. 形式化方法的优缺点4.1. 优点•准确性：形式化方法使用数学和形式化语义描述系统，可以确保规约的准确性和一致性。
•可验证性：形式化方法可以使用数学推理和模型检测等技术对系统进行严格的验证，提高系统的可靠性和正确性。
形式化方法Formal Methods (实例研究)裘宗燕北京大学数学学院2006年2－6月2006年4月2实例1：实时内核问题简介 实时内核进程状态和内核数据结构（原文档） 内核状态后台处理 中断处理 总结2006年4月3简介•嵌入式系统得到越来越广泛的应用•需要一个小操作系统提供进程调度和中断处理功能•嵌入式系统应用有时是安全攸关和生命攸关的•下面的研究是用Z 描述了一个X 光治疗仪的内核•原系统包含大约50 页汇编代码，生成的目标代码将近1K•本研究发现原内核实现有可能出现死锁，当时中断都被禁止，处理器空等待进程的运行–由于实时和并行，这种错误很难通过测试查出并排除–原来的系统错误并没有威胁到病人安全，一个原因是安装了一个限时硬件，以防控制计算机的软件或硬件错误–但这种错误有可能由于系统的修改或者升级而产生严重的后果•这里介绍简化后的这个实时内核规范2006年4月4内核基本情况这是一个典型的用于嵌入式系统的实时内核：•支持后台处理进程和中断处理器•若无中断发生，将有一个后台进程被作为当前进程，处于运行中•当前进程一直运行到自己显式释放处理器，这时调度器将选择另一进程作为当前进程•每个后台进程有一个就绪标志，调度器只在就绪进程中选择•如果一个或几个中断激活，就根据它们的优先级（用一个数表示）选出其中最紧急的中断，令相应的中断处理器运行•中断激活的条件是它们的优先级高于当时已激活的中断，当相应的处理器发出自己已结束的信号时，该中断离开激活状态•后台进程可以注册到某个优先级，使自己变成一个中断处理器图1：内核实现的数据结构（取自原文档）进程，链接成一个环中断控制下的进程调度器控制下的进程ready = trueready = false当前活动进程图2：进程状态被迫转换（其他进程导致）自主转换（自己执行命令）中断控制下的进程调度器控制下的进程箭头反了2006年4月7评价•虽然这种图很常见，但它们的信息可以为应用程序员使用的并不多，其中的许多信息与应用程序员无关，如：–中断处理器和进程连接为一个环，有就绪标志。
这些应用程序员无法检查也不可能利用–调度环只是保证后台进程按固定的顺序运行，应用程序员不能依赖这种情况（否则无法保证应用程序的稳定运行）–图中中断处理器也在环上，也有就绪标志（永远为假），实际上完全可能采用其他实现方式（例如中断处理器从环上取下等）•图2可以看作半形式化描述，把内核描述为一组有穷自动机。
但：–没有给出进程间交互的明确信息（内核需要管理的重要事项）–有些可能状态没有描述（作者举了个例子）2006年4月8内核状态下面开始用Z 做形式化描述。
首先考虑系统的状态空间进程用进程标识符指称，在内核实现中进程标识符是进程控制块的地址。
实际表示形式应用程序员不关心，可以定义为一个抽象集合：考虑定义一个唯一标识符none ，它不是真进程的名字。
当处理器闲置时可以说它正在运行进程none ，其他名字可用于真进程2006年4月9内核状态：后台进程与后台进程相关的状态与调度器有关，定义下面模式：•background ：后台进程的集合•ready ：就绪进程的集合，是调度器选择当前进程时的备选集合•current ：当前进程，可以是none 这里没有说ready 和current 之间的关系2006年4月10内核状态：中断处理器中断用与之相关的优先级表示，优先级是小整数，定义为集合（0 不是中断优先级，作为后台进程的优先级）：中断部分的状态描述为：handler 是部分单射，每个优先级关联至多一个中断处理器，互不相同enable 是允许中断级的集合，active 是当前需要处理的中断级的集合内部状态：内核对于理解内核的工作，有些信息非常关键，如：•没有允许（enable ）的中断就不能激活•不同优先级不能共享同一个处理器这些都是静态的信息，但在程序正文中并没有表现整个内核的状态就是后台和中断两部分的组合：内核状态包括6个变量：内部状态：CPU内核的工作就是确定CPU 运行哪个进程，它属于哪个优先级这两个观察应该看成系统状态的组成部分。
整个系统由CPU 和内核组成下面模式描述CPU 的状态：•当没有进程运行（CPU 运行none ）时running 的值是none •在没有激活的中断，其优先级是0•CPU 的其他状态信息与这里的规范无关（例如寄存器内容，状态寄存器的状态等等2006年4月13内部状态：系统在考虑整个系统的状态时，需要刻画CPU 状态与内核状态之间的关系•如果正在运行后台进程，当时CPU 的priority 必定为0•如果存在激活中断，CPU 一定处于其中最高的优先级，而且正在运行这个优先级的中断处理器下面是描述整个系统状态的模式：易见有：2006年4月14后台进程：启动下面考虑系统状态的变化有些操作只影响状态空间里的后台进程部分，先考虑这部分操作。
操作Start 将一个进程变为后台进程。
用下面模式描述：现有后台进程可以重新Start ，将其置于就绪状态2006年4月15后台进程：释放处理器当前后台进程可以通过调用Detach 操作释放CPU ，下面是相应模式：执行这一操作的前提是当前CPU 运行的是后台进程操作将CPU 置为闲逛状态（执行none 进程），下面的操作将是选择一个新后台进程，或者出现中断2006年4月16后台进程：选择在CPU 闲置时（运行none ），可能自发地执行选择操作。
该操作的模式：•这一操作不属于内核应用程序接口，而是内核的一个内部操作，可以在其前条件满足的情况下随时发生•其前条件是：•规范没说如何选择（抽象性），选择策略（调度策略）是实现的责任•一旦某进程被选中，它一定会立即投入运行，因为当时的优先级为0后台进程：结束后台进程可以自己执行Stop 操作终止，这个进程就结束了：•当时正在运行的必须是一个真正的后台进程•结束的进程从background 和ready 集合里删除•当前进程变为none ，又可能执行Select后台进程：设置就绪/非就绪后台进程可以在就绪和“挂起”状态之间转换，为描述设置进程状态操作，需要先定义一个枚举类型操作的规范：2006年4月19中断处理：注册现在考虑中断处理部分。
一个进程可以把自己注册为中断处理器：本操作只能由后台进程调用。
调用进程从现有后台进程集删除，并注册为指定优先级的处理器（如果原来有，就是取而代之）2006年4月20中断处理：中断处理器硬件保证只有允许的且高于当前处理器优先级的中断才能发生下面模式描述内核在发生中断时的行为：这一模式只说新中断被加入激活中断的集合静态调度模式保证与新中断相关的处理器将开始运行（由系统的priority 确定），下面推导说明新中断的处理器将开始执行：2006年4月21中断处理：新中断因此有：调度策略的其他部分保证：2006年4月22中断处理：结束当一个中断处理器工作完成时，中断处理器调用内核操作IWait ，将自己挂起等待下一次中断。
这个操作的形式描述：只有中断处理器才能执行这个操作（priority > 0）执行操作使当前中断处理器从active 集合中去除，调度策略将自动决定随后执行的中断处理器（或者后台进程）中断处理：撤销另一个操作IExit 结束中断处理器，并撤销它的注册：这个操作使该中断处理器恢复为一个后台进程。
最后两个操作修改允许中断集合，屏蔽或允许中断中断处理：屏蔽2006年4月25原实现的一个错误在原来的实现里，注册操作的实现并不是前面描述的那样，而是：注意这里current' 的定义，这一修改破坏了系统的正确性，因为现在要求必须有另一个就绪的后台进程，调度器将陷入无限循环，去寻找下一个就绪的后台进程（在调度器运行时，将禁止任何中断），导致系统死锁2006年4月26总结•本实例描述了一个实时内核的许多重要方面，但又没有陷入过多的实现细节，如具体数据结构等•这里不仅描述了一个进程执行中可能发生的事件，通过这些事件，进程也可以与其他进程交互，以及与中断交互•但也有一些重要的方面没有包含在这个规范里：–没有模拟进程的状态，进程在释放CPU 时，或者被中断时，必须保存当时的状态，在重新执行时恢复状态–并没有真的描述时间，或者特定时间发生的事件–没有关于进程的调度应该具有某种公平性的描述•其中第一个问题容易解决，只需为每个进程增加状态变量•后面两个问题更困难。
时间信息较难很好地集成在相关描述中，后来有许多人研究带时间的规范，例如有一种带时间的Z 扩充称为TCOZ2006年4月27总结•公平性无法在单一事件的层次上描述，因为它讨论的是系统的长程性质，实际上是无穷事件序列的性质问题。
也可能想出一些描述方法，关键就是重新定义Select•虽然这些问题都可能处理，但加入之后的规范将会复杂许多、难理解许多整理自：Specifying a real-time kernel, Mike Spivey, Oxford2006年4月28实例2：文本格式化工具问题简介 基本概念 文本处理 实现细节 文件 总结问题简介本实例研究描述一个文本格式化程序，它能完成：•普通的ASCII （或者其他字符集的）文本文件的格式化工作，能对各个行做居左、居中和居右的格式编排•实现对于制表符和换行的处理这一规范描述的基本上是Unix 系统里的基本工具pos ，其手册页的基本内容如下（下面的规范并不等价于这一工具。
这种写规范的方式，可以看作是想澄清原工具的各种设计问题，而不是严格的逆向工程）：2006年4月31基本概念现在考虑内容为一些ASCII 字符的文件，定义表示字符的基本集合：空格是一个特殊的字符：行和文档（document ）的抽象可定义如下：字符行是字符的序列文档是字符行的序列有时需要重复一个串若干遍，为此可以扩充Z 语言，利用其功能定义一个运算符，下面通过通用型定义引进一个新运算符2006年4月32基本概念这个定义在下面很有用。
很容易看到这一运算符的许多性质，如：2006年4月33基本概念其中两个很有用的序列运算符定义如下：运算符after 取得n 个元素之后的（子）序列运算符for 取得序列前n 个元素构成的（子）序列2006年4月34文本处理下面考虑文本处理，首先考虑行的处理，而后考虑整个文档的处理。
首先考虑一个函数clipleft ，它删除一行开始的所有空格（如果存在）删除右边所有空格的工作也可以借助上述函数实现：注意：这样描述并不意味着实现中需要这样做写规范时做的是描述操作的性质，实现是后面的工作文本处理：行很容易用它们组合出一个删除两端空格的函数：这两个操作的组合具有下面的性质（可以严格证明）：文本处理下面考虑一行内的位置编排要设定一个行的左端从某个位置开始，也就是在行的开始加入若干空格下面函数完成这一工作：如果一行不是太长，那么就可以将它居中编排，下面函数完成这一工作。
