K语言入门学习6：什么是内建的Integers 和 Booleans

本节课的目的是解释K中两种最基本的，自带的sort：Intsort和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也为Intsort提供了第三个模块:’ 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 ，观察上面表达式的值是如何变化的。为什么会发生这种情况?