软件的形式化

软件概述

• 程序 –> 软件 –> 应用
  • 架构（Architecture）
    • 硬件（Hardware）
    • 外设（Peripheral）
  • 程序（Program）
    • 固件（Firmware）
    • 软件（Software）
      • 系统软件（System Software）
      • 中间件（Middleware）
      • 应用软件（Application Software）
  • 应用软件是一种程序，它通常叫做应用程序（Application Program）
• 软件开发
  • 规范（Specification）
    • 文档（Documentation）
    • 约束（Constraint）
  • 实现（Implementation）
    • 模块化（Modularity）
    • 接口（Interface）
    • 行为（Behavior）
  • 验证（Verification）
    • 测试（Test）
    • 证明（Proof）
• 软件质量
  • 正确性（Correctness）
  • 易用性（Ease of Use）
  • 高性能（High Performance）
• 软件设计的困难之处
  • 层次结构 –> 模块的分解、组合
  • 外部变化 –> 接口、行为的变更
  • 外部相关 –> 软件依赖于其他软件、编程语言、硬件

软件的形式化

• 软件的形式化 –> 代数驱动设计（Algebra-Driven Design）
  • 规范 –> 将软件抽象为代数系统，将约束抽象为公理
  • 实现 –> 根据规范，实现代数系统
  • 验证 –> 根据规范，证明实现满足公理
• 例子——大学课程时间表的应用