本节课的目的是解释K中两种最基本的,自带的sort:Int
sort和Bool
sort,它们分别表示arbitrary-precision integers和Boolean algebra。
K中自带的sorts
K在domains.md中提供了一些有用sorts的说明,可以在K安装的include/kframework/builtin
目录中找到这个文件。这个文件是通过Literate programming风格定义的,我们将在以后的课程中讨论。我们不会立即覆盖所有的sort,但是,这一课讨论了一些关于整数和布尔值的细节,并提供了如何在K的文档中查找更多关于内置函数的详细知识的信息。
K中的Booleans
K提供的最基本的内置sort是Bool
sort,代表着布尔值(即true
和false
)。您已经看到了我们如何能够使用K的解析和消除歧义特性中,自己创建这个类型。然而,在绝大多数情况下,我们宁愿导入由K本身定义好的Boolean algebra。最简单的是,你可以通过在你的定义中导入模块BOOL
来实现这一点。例如(“lesson-06-a.k”):
module LESSON-06-A
imports BOOL
syntax Fruit ::= Blueberry() | Banana()
syntax Bool ::= isBlue(Fruit) [function]
rule isBlue(Blueberry()) => true
rule isBlue(Banana()) => false
endmodule
这里我们定义了一个简单的谓词(predicate),即返回布尔值的函数。现在,我们可以对这些值执行通常的与、或、非等布尔运算。例如(“lesson-06-b.k”):“
module LESSON-06-B
imports BOOL
syntax Fruit ::= Blueberry() | Banana()
syntax Bool ::= isBlue(Fruit) [function]
rule isBlue(Blueberry()) => true
rule isBlue(Banana()) => false
syntax Bool ::= isYellow(Fruit) [function]
| isBlueOrYellow(Fruit) [function]
rule isYellow(Banana()) => true
rule isYellow(Blueberry()) => false
rule isBlueOrYellow(F) => isBlue(F) orBool isYellow(F)
endmodule
在上面的例子中,包含布尔值或是通过orBool
函数执行的,该函数在BOOL
模块中定义。按照惯例,在K中,内置sort上的许多函数都以这些函数定义的主sort的名称作为后缀。这样,K的syntax (通常)就不会与任何其他编程语言的语法发生冲突。
课程练习
编写一个函数isBlueAndNotYellow
来计算适当的布尔表达式。如果您不确定要使用什么syntax,可以参考domains.md中的’ BOOL '模块。添加一个sort为“Fruit”的术语,其中“isBlue”和“isYellow”都返回true,并测试“isblueandnotyellow”函数在所有三个“Fruit”上的行为是否符合预期。
Syntax Modules
对于在domains.md
的大多数sorts, K定义了不少于1个模块,可以被用户导入。例如,对于Bool
sort,K定义了前面已经讨论过的BOOL
模块,但也提供了BOOL-SYNTAX
模块。与BOOL
模块不同,该模块只声明值true
和false
,而不声明任何操作Bool
sort的函数。基本原理是,在某些情况下,您可能希望将此模块导入到您定义的主syntax模块中,而您通常不希望对包含所有Bool
sort函数的模块版本进行此操作。举个例子,如果你是定义的语义c++,你可能会BOOL-SYNTAX
导入的语法模块定义,因为true
和false
是c++的语法的一部分;但只会主要semantics模块中调用BOOL
模块类似的函数,因为c++定义了它自己关于与、或、非运算的语法,它与BOOL
模块中定义的语法不同。
例如,下面是如何重新定义布尔表达式计算器,它使用了“Bool”sort,同时维护模块和导入的惯用结构,并首次包含自主定制计算表达式值的规则(’ lesson-06-c.k '):
module LESSON-06-C-SYNTAX
imports BOOL-SYNTAX
syntax Bool ::= "(" Bool ")" [bracket]
> "!" Bool [function]
> left:
Bool "&&" Bool [function]
| Bool "^" Bool [function]
| Bool "||" Bool [function]
endmodule
module LESSON-06-C
imports LESSON-06-C-SYNTAX
imports BOOL
rule ! B => notBool B
rule A && B => A andBool B
rule A ^ B => A xorBool B
rule A || B => A orBool B
endmodule
请注意syntax的封装:’ LESSON-06-C- syntax ‘模块只包含布尔表达式的syntax,而实现这些函数所需的任何其他语法都在’ LESSON-06-C '模块中。
课堂练习
向上面的布尔表达式计算器添加一个implies
函数,使用’ -> '符号来表示含义。你可以在domains.md
的BOOL
模块中查找K的内置implies
函数。
K中的Integers
不像大多数编程语言,最基本的整数类型是固定精度的整数类型,在K中最常用的 integer sort是Int
sort,它表示数学意义上的整数,即任意精度的整数。
在使用Int
sort时,K提供了三个主要模块用于导入。第一个模块是INT
模块,它包含所有整数的语法以及所有关于整数的函数。第二个模块是INT-SYNTAX
,它只提供整数字面量本身的语法。然而,与K中的大多数内置sort不同,K也为Int
sort提供了第三个模块:’ UNSIGNED-INT-SYNTAX ‘模块。此模块仅提供非负整数的syntax,即自然数。造成这种情况的原因包括词汇歧义。一般来说,在大多数编程语言中,’ -1 '不是一个字面量,而是一个应用一元否定运算符的字面量。因此,K提供了这个模块来简化指定此类语言的语法。
有关Int
sort中可用函数的详细信息,请参阅domains.md
。请再次注意,我们如何在大多数整数操作的末尾附加 Int
,以确保它们不会与其他编程语言的语法发生冲突。
课外练习
- 扩展第1.4课第2题的解决方案,实现定义加、减、乘和除行为的规则。让用户不要担心此时试图除以零的情况。使用
/Int
实现除法。通过执行作为第1.3课第2题一部分编写的算术表达式来测试新的计算器实现。检查以确保每个计算的值都是您期望的。 - 将本课所学的布尔表达式计算器与问题1的解决方案结合起来,然后将组合计算器扩展为
<
,<=
,>
,>=
,==
和!=
的表达式。编写一些布尔表达式,组合整数和布尔操作,并测试以确保这些表达式返回预期的真值。 - 用问题2的解计算以下表达式:
7 / 3
,7 / -3
,-7 / 3
,-7 / -3
。然后将定义中的/Int
函数替换为divInt
,观察上面表达式的值是如何变化的。为什么会发生这种情况?