DTRC等价性的形式自动证明的任务书任务书：DTRC等价性的形式自动证明背景：在计算机科学领域，等价性的判定一直以来就是一个重要的问题。在软件、硬件设计等领域，等价性检测是十分关键的工作，它可以帮助人们判断两个系统或者两个程序是否等价。目前，很多等价性工具已经应用于软件开发和硬件设计中。任务：该任务要求编写一个程序，可以对两个循环程序进行等价性的判定，即判断这两个程序是否具有等价的循环结构和语义。设计要求：1.对两个循环程序进行抽象语法树的自动化建立。2.基于程序的抽象树，设计出自动证明等价性的算法，并实现该算法。3.考虑程序的不同语法和语义，例如循环条件、循环次数等因素。4.程序能够输出程序等价性的证明结果。参考文献：1.《计算机程序设计与证明：等价性检测》；2.《计算机程序的自动等价性检测方法研究及应用》；3.《程序等价性检测方法综述》。评估标准：1.完成DTRC等价性的自动化证明；2.代码实现质量；3.完整的程序测试和输入输出文件；4.代码的可维护性和可扩展性；5.文档质量。