软件形式化 可信软件

发布日期：2020-08-25

关系数据结构及形式化定义有什么？

计算机科学和软件工程领域编辑形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证.将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和鲁棒性.但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统.2逻辑科学编辑形式化是指分析、研究思维形式结构的方法.它把各种具有不同内容的思维形式（主要是命题和推理）加以比较，找出其中各个部分相互联结的方式，如命题中包含概念彼此间的联结，推理中则是各个命题之间的联结，抽取出它们共同的形式结构；再引入表达形式结构的符号语言，用符号与符号之间的联系表达命题或推理的形式结构.例如，把全称肯定命题，用符号形式化为“SAP”；把联言命题、假言命题分别形式化为：“p∧q、“p→q”.又例如：一个具体的假言联言推理“如果这种金属是纯铝，那么它的物理性质必与纯铝相同；如果这种金属是纯铝，那么它的化学性质必与纯铝相同；但这种金属的物理性质和化学性质与纯铝不相同；所以，它不是纯铝.”这个推理的形式结构是：“如果p，则q；如果p，则r；非q且非r；所以非p.”可进而形式化为下列公式：（（p→q）∧（p→r）∧┐q∧┐r→┐p.

“软件构造”究竟是什么意思？

软件构造的一般原则（模块设计、代码重用、类设计等）软件构造的常用技巧（契约式设计、防御式编程、异常处理、配置式编程、基于状态转移和基于表的软件设计、基于语法分析的设计等）软件构造的形式化方法（规范说明语言及其应用、形式化构造工具），软件构造工作的执行要点（编码及其规范、工具使用、单元测试技巧、性能优化等）。