函数和实例

函数

TLA+中除了数字，字符串，布尔值，模型值 4种基本类型外，还有两种复杂类型，分别为集合和函数。函数构成了所有实用复杂类型的基础。

函数的形式看起来跟之前介绍过的操作符是一样的。函数定义的两种方式：

Function == [s \in S |-> foo]  \* 这里foo可以是任何方程式。注意这里用的是|->，不是:
Function[s \in S] == foo

在函数定义中可以使用无限集合，如

Doubles == [n \in Nat |-> 2*n ]
Doubles[12] = 24 \* 调用方式为[],而不是()\* 多参数
Sum == [x, y \in 1..10 |-> x + y] \*限定了x,y的值在1..10中
Sum[2,3] = 5
Sum[2,30]    \* error，30不在1..10中Addx(x) == [y \in Nat |-> x+y+1]
Addx(2)[3] = 6  \*该调用x=2,y=3

函数集

函数集的语法为：SetOfFunctions == [A -> B]，注意这里用的是 -> ,而不是|->。 ->的结果需要用|->来描述。例如：

S1 == {1, 2}
S2 == {3, 4}
[s \in S1 |-> S2] = [1 |-> {3, 4}, 2 |-> {3, 4}] = <<{3,4},{3,4}>> \* 这是一个元组
[S1 -> S2] = {[1 |-> 3, 2 |-> 3], [1 |-> 3, 2 |-> 4], [1 |-> 4, 2 |-> 3], [1 |-> 4, 2 |-> 4]} = {<<3, 3>>, <<3, 4>>, <<4, 3>>, <<4, 4>>} \* 这是一个集合，[1 |-> 3, 2 |-> 3]中的1表示第一个元素，2表示第二个元素，如果将1,2替换为2,3，就不能表示为<<3,3>>了，只能表示为[2|->3,3|->3]

实例

1、给定一个字符串，返回每个字符的个数。如：给定<<“a”,“b”,“a”>>返回 [a |-> 2, b |-> 1]

\* 1 将元组转化为集合，此时集合中包含了不重复的元组的元素 2 遍历集合元素，统计每个元素在元组中的个数
Range(S) == {S[t]:t \in 1..Len(S)}
Counter(str) == [c \in Range(str) |-> Cardinality({n \in 1..Len(str) : str[n] = c})]Counter(<<"a","b","a">>) = [a |-> 2, b|-> 1]

2、给定一个集合S和数字N，返回N个S的笛卡尔积，如Op(S, 3) == S \X S \X S

Op(S,N) == [1..N -> S]

通过例子学TLA+(十二)-- 函数与实例相关推荐

通过例子学TLA+(十五)--时序属性
时序属性 Termination 最简单的时序属性是Termination,Termination是算法终止的要求,如果算法崩溃或者死锁或者进入一个无限循环,那么久违反了Termination规范. ...
通过例子学TLA+(十四)--宏，过程与标签
宏,过程与标签 TLA+在多进程之间复用代码,最简单的方法是使用宏和过程. 宏宏是通用的代码内联器,格式为 nacro Name(var1,...) begin\* stuff end macro; ...
通过例子学TLA+(十)--集合
集合集合用大括号来表示,如{1,2},对于连续的数字集合有种特殊的表示方式,如 1-3 表示集合{1,2,3} 下表是集合的常见操作 Operator example 备注 \in 1 \in {1 ...
通过例子学TLA+(二) -- DieHard
第二个例子DieHard 这是一个倒水的例子,初始一个3升容量的桶,一个5升容量的桶,水不限,如何倒出一个容量刚好是4升的水.在一部老电影DieHard中主角就面临这个问题,这里就将module名命名 ...
深入理解PHP内核(十二)函数-函数的定义、传参及返回值
原文链接:http://www.orlion.ga/344/ 一.函数的定义用户函数的定义从function 关键字开始,如下 function foo($var) { echo $var; } 1 ...
零基础入门python3.7 ——基础知识总结(十二) 函数进级
python中的函数调用时除了对位传参. 关键字传参. 默认参数以外还提供了以下传参方式. 一.可变参数顾名思义可变参数就是参数的个数是可变的,可以是任意1个或者多个,由于参数的数量不确定所以我们要 ...
通过例子学TLA+(十三)--多进程与await
多进程之前使用的例子都是单进程的,现在用多进程来描述多个逻辑同时发生,TLA+中的多进程可以理解为其他高级语言中的多线程.为了方便理解,使用Pluscal语言来描述,TLA+ Toolbox可以将p ...
通过例子学TLA+(七)--操作符
Operator TLA+中的操作符类似于其他编程语言中的函数或者宏定义,使用 == 来定义,例如 Five == 5 \* 无参数时不用加括号 Sum(x,y) == x + y SumwithFi ...
【C语言进阶深度学习记录】三十二函数指针与使用函数指针实现回调函数
回调函数是非常重要的概念文章目录 1 函数的类型 2 函数指针 2.1 函数指针的使用 2.2 使用函数指针实现回调函数 3 总结 1 函数的类型跟以前学数组的时候是一样的,C语言中的数组是有自己 ...

通过例子学TLA+(十二)-- 函数与实例

函数和实例

函数

函数集

实例

通过例子学TLA+(十二)-- 函数与实例相关推荐

最新文章

热门文章