形式化方法—作业1—环境安装及语法树实现

一.背景

  课程主页: Formal Methods Foundation
  作业地址: Formal Methods Assignment1
  如果您的英文足够好,请直接点击上述链接查看相关信息
  由于课程结束上述链接失效, 请点击此处Wolai课程链接查看相关资料。

二.作业

 2.1环境安装

  安装Coq,请参考: Coq安装
  安装z3
  直接在PyCharm中安装即可,安装下图中的z3和z3-solver即可

  如果您的安装速度过慢甚至停滞不前,请参考: PyCharm换源

 2.2内容

  在Python中实现一个非常简单的算术计算器
  计算器语言的语法由以下上下文无关语法 (CFG) 描述:
  exp ::= num
    | exp + exp
    | exp - exp
    | exp * exp
    | exp / exp
    | (exp)
  上面的 CFG 生成的表达式可以用树表示。例如,表达式3 * 4 + 10 / 2的AST如下:


            +
          /   \
         /     \
        *       /
       / \     /  \
      /   \   /    \
     3    4  10     2 

 2.3 代码实现

import unittest

class Todo(Exception):
    def __init__(self, msg):
        self.msg = msg

    def __str__(self):
        return self.msg

    def __repr__(self):
        return self.__str__()

#表达式类
class Exp:    
    def __repr__(self):
        return self.__str__()

#原子表达式 exp ::= num
class ExpVar(Exp):
    def __init__(self, value):
        self.value = value

    def __str__(self):
        return str(self.value)

#加法表达式 exp = exp + exp
class ExpAdd(Exp):
    def __init__(self, left, right):
        self.left = left
        self.right = right

    def __str__(self):
        return f"{self.left} + {self.right}"

#减法表达式 exp = exp - exp
class ExpMinus(Exp):
    def __init__(self, left, right):
        self.left = left
        self.right = right

    def __str__(self):
        return f"{self.left} - {self.right}"

#乘法表达式 exp = exp * exp
class ExpMulti(Exp):
    def __init__(self, left, right):
        self.left = left
        self.right = right

    def __str__(self):
        return f"{self.left} * {self.right}"

#除法表达式 exp = exp / exp
class ExpDiv(Exp):
    def __init__(self, left, right):
        self.left = left
        self.right = right

    def __str__(self):
        return f"{self.left} / {self.right}"

#括号表达式 exp = (exp)
class ExpPar(Exp):
    def __init__(self, value):
        self.value = value

    def __str__(self):
        return f"({self.value})"

     
def eval_value(exp: Exp):
    #原子表达式,直接获得变量值,转换为int类型
    if isinstance(exp, ExpVar):                   
        return int(exp.__str__())
    #括号类型由于只有一个值,单独处理
    if isinstance(exp, ExpPar):                  
        return eval_value(exp.value)

    #分别求出左右表达式对应值
    a = int(eval_value(exp.left))
    b = int(eval_value(exp.right))              

    #根据表达式类别递归求解
    if isinstance(exp, ExpAdd):                   
        return a + b
    if isinstance(exp, ExpDiv):
        return a / b
    if isinstance(exp, ExpMulti):
        return a * b
    if isinstance(exp, ExpMinus):
        return a - b

#测试用例1
test_case_1 = ExpAdd(
    ExpMulti(ExpVar(3), ExpVar(4)),
    ExpDiv(ExpVar(10), ExpVar(2))
)

#测试用例2
test_case_2 = ExpMinus(
    ExpMulti(
        ExpPar(ExpAdd(ExpVar(12), ExpVar(217))),
        ExpVar(3)
    ),
    ExpVar(621)
)

class TestTableau(unittest.TestCase):

    def test_print_1(self):
        self.assertEqual(str(test_case_1), "3 * 4 + 10 / 2")

    def test_print_2(self):
        self.assertEqual(str(test_case_2), "(12 + 217) * 3 - 621")

    def test_eval_1(self):
        self.assertEqual(eval_value(test_case_1), 17)

    def test_eval_2(self):
        self.assertEqual(eval_value(test_case_2), 66)

if __name__ == '__main__':
    unittest.main()

#测试结果
#Ran 4 tests in 0.002s
#OK

三.下载链接

  在线下载: 请点击这儿下载
  如果下载失败,点击此百度云链接:形式化方法作业一,提取码y825

end
  • 作者:Yuan(联系作者)
  • 发表时间:2021-11-29 20:15
  • 版权声明:自由转载-非商用-非衍生-保持署名(创意共享3.0许可证)
  • 转载声明:如果是转载博主转载的文章,请附上原文链接
  • 公众号转载:请联系作者
  • 评论