软件工程期中试卷：形式化方法与Z语言实践

"苏州大学计算机科学与技术学院的软件工程课程关于软件形式化的期中试卷，涵盖形式化方法的基本内容、函数表示、序列处理、进程调度、二叉树操作及用户登录系统的Z语言规约设计。试卷以闭卷形式进行，适合05、06级软件工程专业的学生复习备考。" 此期中试卷主要测试了以下几个关键知识点： 1. **形式化方法**：形式化方法是软件开发中的一种严谨方法，它通过数学公式和逻辑来精确地描述软件需求和设计。它包括建模语言、证明技术和验证技术，用于确保软件的正确性和可靠性。在软件工程中，形式化方法可以减少错误，提高软件质量，特别是在安全关键领域的应用。 2. **λ表示法**：λ表示法是一种函数表示方式，源自λ演算，用于无类型的函数定义。在题目中，考生需要使用λ表示法定义一个取三个整数x、y、z并返回它们中最小值的函数。 3. **Z语言**：Z语言是一种形式规格说明语言，用于精确描述软件或系统的逻辑行为。题目要求使用Z语言来规约序列处理（去除重复元素并按出现次数排序）和进程队列（CPU调度）的操作。 4. **进程调度**：考生需要设计一个Z语言规约的进程队列，其中包含CPU调度策略，如优先级排序和特殊进程(idle)处理。 5. **二叉树**：设计一种二叉树结构，每个节点都有权重，实现中序遍历和左右子树权重调整的操作。中序遍历是一种树遍历方法，通常用于打印排序二叉树的有序序列。而交换左右子树是为了保持特定的权重平衡条件。 6. **系统登录与用户管理**：使用Z语言规约一个系统LogSys，涉及用户注册、注销、登录、修改口令、退出系统以及两种身份（游客和注册用户）登陆的逻辑。这是对数据库操作和权限控制的理解和应用。 这六个问题覆盖了软件工程中的核心概念，包括形式化方法、函数表示、数据结构、算法设计、进程管理以及系统模型化，旨在评估学生对软件开发理论和实践的综合理解。通过解答这些问题，学生能巩固并深化他们在软件工程课程中学到的知识。