形式方法--讲义1.ppt

1、,Formal Methods (1),形式方法课程教学大纲,课程的英文名称：Formal Methods 课程编号： 总学时： 72 学分：4 适用对象：BTEC专业 先修课程：计算机平台,1.Description of unit Specification of secure and well-engineered computer systems requires the unambiguous, concise and provable language of mathem-atics. This unit aims to acquaint learners with the mat

2、hematical concepts and notation that underpin formal methods, such as Z （软件工程中的Z方法：Z语言是一种基于集合和一阶谓词逻辑的模式规约语言,可用于产生精确的需求规格说明。）, set theory and propositional and predicate logic and functions集合论，命题逻辑和谓词逻辑，函数. The unit also gives learners experience of proof by induction (a principle of functional progr

3、amming) and relationship matrices数学归纳法证明和关系矩阵. The latter, as well as reinforcing set and logic theory, will provide an alternative application of the rules of matrix algebra.,1 Employ the laws of set algebra, propositional logic and predicate logic,solve set theory problems using Venn diagrams（利用文氏

4、图解决集合问题） simplify compound logic statements using truth tables and appropriate simplification techniques（利用真值表或通过适当化简解决复合逻辑问题） apply universal and existential qualifiers（利用通用和现有的可行方法）,2 Solve problems using mathematical induction, relationships and functions,perform mathematical induction（数学归纳法的应用）

5、produce combinations of Boolean relationship matrices（关系矩阵及其运算） understand functional notation（函数概念及其应用）,3 Understand formal methods schema,apply formal methods schema（形式方法模式应用） apply set theory, logic and function notation（集合、逻辑和函数模式的应用） evaluate the importance of using formal methods schema（评价所使用的

6、形式方法）,3.Content 3.1. Set algebra, propositional logic and predicate logic(代数集,命题逻辑,谓词逻辑) Set theory（集合）: notation (null, universal, complement, subset, element空集，全集，补集，子集，元素), set operations (union, intersection, subtraction集合运算：并，交，差), laws of set algebra（集合代数法则）, Venn diagrams（文氏图）, power set（幂集）,

7、Logic（数理逻辑）: definition of proposition（命题的定义）, propositional logic laws (and, or, not, eor, equivalence, implication)（命题逻辑）, laws of propositional logic, tautologies（重言式）, truth tables for compound statements（真值表）, simplification of logic expressions（逻辑表达式及其化简）, predicate logic (universal and existe

8、ntial qualifier)（谓词逻辑：全称量词和存在量词）,3.2. Mathematical induction, relationships and functions Mathematical induction: principles of induction（数学归纳法）, sigma notation（累加符号）, solution of induction problems linked to recursion（递归） Functions（函数）: notation for relation（关系）, definition of a function（函数定义）, map

9、pings of functions（映射）, function domains（函数定义域和值域）, inverse functions（反函数）, two state (Boolean) matrix representation and solutions（矩阵）,3.3. Formal methods schema（形式方法模式） Schema layout: predicate and signature, schema notation Schema conventions: expressions（表达方法） Schema interpretation: the producti

10、on of written descriptions/pseudocode that represent a formal methods specification （利用描述方法或伪代码方法描述问题。）,3.4. Formal specifications （形式规范） Use of formal specifications: benefits, features, reliability（好处，特点，可靠性） Importance in critical systems: human safety, high cost related systems（性价比）,4 Understand

11、 the use of formal specifications,identify suitable use of formal specifications（学会识别、选择合适的形式方法） justify the use of formal specification（证明所使用的形式方法是正确而有效的）,Logic,There are various types of logic such as logic of sentences (propositional logic命题逻辑), logic of objects (predicate logic谓词逻辑), logic invol

12、ving uncertainties不确定性, logic dealing with fuzziness模糊性, temporal时态性 logic etc. Here we are going to be concerned with propositional logic and predicate logic, which are fundamental to all types of logic.,研究人的思维形式和规律的科学称为逻辑学，由于研究的对象和方法各有侧重而又分为形式逻辑、辨证逻辑和数理逻辑。 数理逻辑是应用数学方法研究推理的科学。数理逻辑又叫符号逻辑，因为它的主要工具是符号

13、体系。数理逻辑的核心是把逻辑推理符号化，即变成象数学演算一样完全形式化了的逻辑演算。,1. proposition,Contents Sentences considered in propositional logic are not arbitrary sentences but are the ones that are either true or false, but not both. This kind of sentences are called propositions. If a proposition is true, then we say it has a trut

14、h value of true; if a proposition is false, its truth value is false. 简言之，命题是非真即假的陈述句。,For example Grass is green, and 2 + 5 = 5 are propositions. The first proposition has the truth value of true and the second false. But Close the door, and Is it hot outside ?are not propositions.,Also x is greate

15、r than 2, where x is a variable representing a number, is not a proposition, because unless a specific value is given to x we can not say whether it is true or false, nor do we know what x represents.,Similarly x = x is not a proposition because we dont know what x represents hence what = means. For

16、 example, while we understand what 3 = 3 means, what does Air is equal to air or Water is equal to water mean ?,Does it mean a mass of air is equal to another mass or the concept of air is equal to the concept of air ? We dont quite know what x = x mean. Thus we can not say whether it is true or not. Hence it is not a proposition.,Elements of Propositional Logic,Simple sentences which are true or false are basic propositions.原子命题 Larger and more complex sentences复合命题are constructed from basic propositions by combining them with connectives.命题联结词 Thus propositions and connect