面向对象JML实战：地铁系统与Path/RailwaySystem实现

本次面向对象JML系列第三次作业的主要目标是提升对JML规格进阶级的理解和实际应用，同时掌握设计模式及单元测试的高级实践。作业的核心内容涉及两个关键类的实现：Path 和 RailwaySystem。Path 类作为一个容器，需要支持路径的增删查改操作，以及基于无向图的查询。而 RailwaySystem 类则代表了一个简单的地铁系统，能够处理路径相关的查询，包括线路之间的换乘计算和票价计算。 具体任务要求学生继承官方提供的 Path 和 RailwaySystem 接口，并自定义实现 MyPath 和 MyRailwaySystem 类。这些类需要严格遵循给出的 JML 规格，这包括接口中的方法定义及其行为描述。JML (Java Modeling Language) 是一种静态分析工具，用于规范接口的行为，确保代码质量和一致性。 设计模式在这个过程中可能会被应用，例如可能涉及到工厂模式或者策略模式，以提供灵活的方式来创建和管理地铁线路。学生需要根据提供的接口源代码和JML规格，编写出高效且易于维护的代码。 单元测试是另一个重要的环节，学生们需要编写针对自己实现的类的测试用例，确保每个接口方法的正确性和性能。这有助于发现潜在的问题，并验证代码是否符合预期的行为。 在主类中，学生需要调用官方提供的 AppRunner 类，并加载自己实现的 MyPath 和 MyRailwaySystem 类，以便构建完整的可运行程序。这展示了如何将类实例化并与主程序集成，实现功能的交互。 对于地铁系统的概念，换乘是指从一条线路转移到另一条线路时在同一个站点发生的切换。计算票价时，需要考虑经过的边数和换乘次数。例如，在路线2->3->5中，经过2条边，一次换乘，所以票价为边数加上换乘数，即2+1=3。 作业完成后，除了技术技能的提升，学生还将获得关于抽象和接口设计、代码规范性以及测试驱动开发的实践经验。不满意度部分可能用来评估学生对规格理解和实现的准确性，以及他们如何处理可能出现的问题和优化代码质量。这个作业是一个综合性项目，旨在强化学生的面向对象编程、设计模式理解和单元测试实践能力。