95理论计算机科学电子笔记64（2002）网址：http://www.elsevier.nl/locate/entcs/volume64.html18页定时项重写系统Jer emieBlanc and RachidEchahedLeibniz{Institut IMAG，CNRS46，avenue F Viallet，F-38031 Grenoble，France电话：（+33）4 76 57 46 73;传真：（+33）4 76 5746 02@ imag.frRachid. imag.fr摘要我们提出了一类新的重写系统，它是一阶条件项重写系统的保守扩展，以及时间特征，如时钟，信号，定时项，定时原子和定时规则。本文首先根据时间项重写系统的语法定义了它们，并通过一些例子进行了说明。然后，我们提供了一个语义标记的过渡系统的基础上。最后，我们将展示我们的框架与相关工作的比较。1介绍术语重写系统在过去几年中得到了广泛的研究[5，11，6]。它们是许多现代声明性语言、定理证明器和程序验证技术的基础。这项工作的主要动机来自于观察，长期重写系统未能指定在一个自然的方式在现实世界中的应用程序，其中涉及的时间。实际上，考虑例如布尔运算符Alarm与以下prole设备排序！bool，这样每当设备被破坏时，Alarm（device）都为true，最后十秒不幸的是，这样简单的程序不能严格使用经典的重写系统来描述。在本文中，我们引入定时项重写系统作为一类新的重写系统，它允许一个指定声明性的应用程序的时间的概念，应该是定性或定量的，涉及。我们的方法是新的，并且偏离了已经提出的建议，以便为一些声明性语言（如tcc[16]，Templog[1]和Chronolog[19]）添加时间。粗略地说，定时重写系统提供有用户定义的和传入的信号，如同步语言，例如[9]。信号是随时间发生的对（tick，值）的流。我们假设给定一个规范信号或时钟，标记为Ref，其用作其他信号的参考。通常，定时重写系统或程序P内的操作符定义可以取决于时间。因此，在Ref的每个时刻t， ac 2002年由Elsevier Science B出版。诉在CC BY-NC-ND许可下开放访问。Blanc，Echahed96新的重写系统由操作符定义组成，以与数据流语言相同的方式更新。然后，我们得到重写系统流，F0;F1;：;Ft;：。在任何时刻t，Ft构成可以照常使用的经典重写系统，例如，公式的简化或分解为了使这种定时重写系统的描述更容易，我们丰富了第一阶术语的时间操作符，在这是用来指过去的定义。例如，表达式at（3seconds）f（0）+f（1）意味着将现在之前三秒的f（0）值与当前时刻的f（1）值相加。另一方面，我们也丰富了经典原子，允许使用的方块2和钻石3模态算子的时间间隔。一个定时原子2IB，分别为3IB，保持i，原子B在时间间隔I的每个时刻，分别为至少一个时刻保持。我们在本文中考虑的重写规则具有以下一般形式lhs！trhs（主体，当尾时，其中lhs（相应trhs）是一个术语（resp.时间项）表示左手侧（相应地，右手边）的规则，体和尾是可能定时原子或方程的合取尾部的作用是在每一时刻t过滤构成重写系统Ft的重写规则。本文的其余部分组织如下。下一节将介绍定时重写系统的类别，并提供示例来说明我们的框架。然后，我们提出了一个语义标记的过渡系统的基础上，我们的程序。在第4节中，我们将我们的建议与相关工作进行了比较。第五节指出了操作语义学的一些相关问题，并对全文进行了总结。2定时重写系统我们将定时重写系统或程序定义为一对P =其中是定时的第一阶签名，并且R是定时的条件重写规则的集合。一个时间一阶签名是一个三元组S ; S ; >，其中S是一个排序集，S是一个S+排序的信号族，S是一个S+排序的时间算子族。S+表示S上的非空字符串集合。我们假设S至少包含布尔类型的bool和自然类型的nat。在我们的方法中，信号的含义与一些同步语言中引入的含义非常接近，例如，[9，7]。s1;：; s n; s的信号s，记为s：s 1;：; s n！s是操作符表示的流。这些表示隐式地关联到随时间的一些时刻。这些瞬间构成一个集合，称为s的滴答。因此，我们的时间概念是线性的和多形式的. 每一个信号都与一个记录在案的操作员相关联！s，其中在所考虑的信号s的滴答上，h等于真。族S包含我们称为参考信号的区别信号，参考信号为Prole Ref：！更确切地说，Ref是嵌套信号，即对于S中的所有信号s，s的滴答被映射到Ref的滴答中。一 开始，Blanc，Echahed97Ref的值为0，则它在每个时刻递增1它的值可以用作时钟，给出当前时刻的数字。从定时签名开始，我们引入了定时项的概念，以考虑由于信号的存在而导致的运算符的“临时化”。运算符的定义，比如说！，每时每刻都在改变我们利用一个特殊的时间算子来引用算子的过去定义，它是对Lustre [7]中的前算子和Signal [9]中的$算子的推广。我们写在（ns）！请咨询接线员！在对应于当前时刻之前的信号S的n个滴答的时刻。一般来说，我们可以使用几个at表达式来定义运算符过去的正确时刻为此，我们使用定时运算符表达式或简称toe，如下所示：--=！（ns）在哪里！是一个算子，n是一个正自然数，s是一个信号，是一个脚趾。在（ns）处的形式的趾称为过去趾。时间项通过引用算子的过去定义扩展了经典的时间项。其定义如下：tt：：= x j（u 1;：; u m）其中x是一个变量，m是一个自然数（m 0），是一个toe，u1;：; um是有序的时间项。R 中 的 公 式 是 以下形式的 定 时 条 件 重 写 规 则 ： lhs！ trhs（B，当C其中lhs是一阶项，trhs是时间项，B和C可能是时间原子的空连接。lhs！trhs被称为头、B体和C尾。一个时间原子或者是一个方程u 1 == u 2其中u 1和u 2是两个时间项，a对于mula3 j1b1. b2j2B0，其中当定时原子B0在intervalj1b1.期间为真至少一次时成立。 b2j2，或a对于mula2 j 1b1. b2j2B0，当定时原子B0在每一时刻都为真时，b2j2B0成立。 b2j 2. 一种形式为2 j 1b1的符号。 b2j 2B0（分别为3 j 1b1. b2，b2，b0）被称为金刚石原子（特别是金刚石原 子 ）。 j1和j2代表符号[或符号]，表示边界是否包括在区间中，而b1和b2代表标记为ns的对，其中n是非空自然数，s是信号。我们也用“now”作为b2的一种特殊形式来表示当前时刻。尾部的作用是在每一个时刻选择要考虑的重写规则。定时程序P生成经典（非时间）重写系统的不间断序列Ft，也称为续篇中的存储直观地，在每个时刻t，F t包括所有重写规则，使得当C在P中并且C在t处保持时。由于尾部是定时原子的合取，因此空的（或缺失的）尾部总是被认为是真的。现在我们介绍一些我们在续篇中使用的技术定义和符号我们写F`B是为了说明原子B在经典重写中成立，Blanc，Echahed98PP程序P. 为了每个操作员！0o发生在Defc（！），Defc（！）conntainsP.. ... .F0F1FtFig. 1. 商店生成系统F. 我们说一个定时重写规则定义了一个操作符！ 如果！ 是最外面的操作员的左手边的头部。我们注意到DefP（！），设定定时重写规则的德宁运算符！然而，Def P（！） 不是独立的，因为它可能包含一些操作器！这里面没有定义。因此，我们引入符号Defc（！）对于定时重写规则的集合完全定义一个运算符！按同步的P PP de ning的定时重写规则！0的情况。我们打电话给临时工，接线员！的定时程序P，使得Def c（！）不包含任何对计时语法实体的引用。请注意，经典的术语重写系统仅由术语操作器定义组成。我们注意到Rf！ ！ ！0 g为定时操作员更换的结果！由一个定时操作员！0的时间重写规则的集合R中。下面我们给出一些玩具例子来说明我们的框架。例2.1（斐波那契数列）在这个例子中，我们给出了Fibonacci函数的两个不同定义。 这个函数通常用来显示同步语言的能力。 在我们的框架中，我们可以通过遵循syn-statement风格（b1）或纯声明风格（b2）来定义Fibonacci函数。然而，b1将是一个定时运算符，其值将在执行过程中改变，而b2将是一个非时态运算符。1.b1！0，当Ref ==0时2.b1！ 当Ref == 1时为13.b1！at（1Ref）b1 + at（2Ref）b1当Ref> 1 == true1. b2（0）！ 02. b2（1）！ 13. b2（x）！b2（x-1）+b2（x-2）（x> 1 == true实施例2.2（蒸汽锅炉）这个例子是从[4]中得到启发的。 目的是维持水位在蒸汽锅炉中，尽可能在低水位和高水位两个极限之间。在没有任何干预的情况下，由于蒸汽的流出，该水平正在下降。nat排序的输入信号流的值提供当前Blanc，Echahed99测量的蒸汽，并且NAT分类的输入信号电平的值提供了当前测量的水位。如果液位超出区间[低液位;高液位]超过5个瞬间，则必须触发报警。 每当布尔信号报警的新滴答发生时，实际报警被触发。报警的定义是：警报！当2 [5Ref：：now [level > high level == truealarm！truewhen2[5Ref：：now[level low level == true注意alarm的值总是true。这不是一个问题，因为我们只对信号报警的滴答声感兴趣，也就是说，！警报 只有当上述两个尾部之一成立时，此值才等于true。水位的控制是通过四个泵来执行的，泵1、泵2、泵3和泵4都是相同的。泵1，泵2，泵3和pump 4是排序pump排序的非时态算子，P是nat排序的这些泵向蒸汽锅炉供水，以补充排出的水蒸汽。它们是由一个信号泵控制的，顺序排列的亲泵排序！泵顺序排序。数据类型pump order sort由两个构造函数组成，比如on和o。当发生泵命令的滴答声时，命令被发送到泵。 泵指令（P）==开意味着泵p必须工作，泵指令（P）==0意味着泵p必须空闲。我们假设订单在下一个瞬间之前被执行而没有失败。此外，工作应在泵之间公平分配因此，泵命令的值取决于两个参数：所需的数量req_pump_nb_of_pumps_to_on以及泵之间的公平性条件最后一个参数是通过对泵进行排序来实现的，该排序由（泵的）列表或泵列表给出。这样的列表的第一个元素表示要被选择以在下一时刻执行所需工作的第一个泵。顺序泵列表被划分为工作泵和静止泵两个列表，休息泵）是应该工作的泵的列表（分别在下一个瞬间。顺序泵列表是一个信号的prole泵排序列表。工作泵和休息泵是prole pumpsort list的定时操作器Req Pump NB是Prole Nat的定时算子每当工作泵列表被修改时，我们将订单发送给属于工作泵的每个泵，并发送给其他泵。因此，泵浦顺序的定义为：Pumporder（p）！如果在（p，工作泵），则在else上，当工作泵6= at（ 1Ref）working pumps == true工作泵的泵列表是顺序泵列表的前x，使得该前x的长度是所需的泵数量req pump nb。相反地，静止泵的泵列表是顺序泵列表w.r.t.中剩余的补充泵列表。工作泵。工作泵的定义和Blanc，Echahed100静止泵（operator pre x和delete pre x很简单）：工作泵！ 前x（请求泵号，订购泵列表）时！订单泵列表== true休息泵！删除前x（请求泵编号，订购泵列表），当！订单泵列表== true另一方面，req pump nb的值取决于测量的蒸汽量（steam）以及测量的水位（level）。当水位高于高位时，我们需要降低水位。因此，所需的工作泵的数量req pump nb是蒸汽在外部水P上分配的结果。当水位低于低水位时，我们需要升高水位。因此，工作泵的所需数量req pump nb是蒸汽除以P的结果，加1。因此，由于计算所需泵的数量的公式根据水位的位置而不同，我们使用prole nat！nat在每一个时刻选择要考虑的正确公式。请求泵nb！请求泵fct（蒸汽）需要泵功能！s div Pwhenlevel > high level == true需要泵功能！（s div P）+1当电平低电平== true时请注意，以下定义引入了一种计算所需泵数的方法，该方法与[4]中的方法不同，因为即使level在低电平和高电平之间，req pump nb也会在每个时刻计算到最接近的便士我们用来确保在泵之间公平分配工作的策略包括在固定的持续时间d内轮流使用泵，其中d是自然数。工作较多的泵（分别为 少于）d个时刻被所述应变（分别地，新鲜的）。《易经》的卦名，新鲜）泵通过应用于工作泵来计算，函数应变（分别为 新鲜的）。这些功能都是定时操作的亲乐泵排序列表！泵分类名单由于泵会立即对订单做出反应，因此泵的当前状态由我们发送的最后一个订单给出因此，从泵列表中进行应变提取，泵p的子列表使得2 [dRef：：now [pump order（p）== on。strained（[]）！[客户端]strained（p：：l）！（1）A（2 [dRef：：now[pump order（p）== onstrained（p：：l）！（1）（1）（3 [dRef：：now[泵顺序（p）== o类似地，从泵列表中提取新鲜的提取物，泵p的子列表，Blanc，Echahed101这3[dRef：：now[泵顺序（p）==o：fresh（[]）！[客户端]fresh（p：：l）！p：：fresh（l）（3 [d Ref：：now[pump order（p）== ofresh（p：：l）！新鲜（l）（2[dRef：：now[pump order（p）== on现在我们准备好了新的泵列表。它是通过附加（+）以下三个列表构建的：Fresh（at（1Ref）working pumps）代表仍然新鲜的工作泵，在代表当前空转泵的（1Ref）静止泵处，应变（在（1 Ref）工作泵处），其代表当前的应变泵。当我们需要设置的泵的数量请求泵nb 6=在（1参考）请求泵nb== true）或者某些工作泵是应变的（即，应变（在（1参考）工作泵）6=[]==真）。订购泵列表！当Ref== 0时，[泵1;泵2 ;泵3 ;泵4]订购泵列表！新鲜（在（1个参考）工作泵处）+在（1参考）静止泵+应变（在（1参考）工作泵）时，要求泵nb 6=在（1参考）要求泵nb或（strained）at（ 1Ref）working pumps））6= [] == true3标记转换系统我们假设在续集中，定时重写系统P是给定的签名.如图1所示，程序P的一次运行产生一个存储流，F0; F1;：; Ft;等等。在本节中，我们精确地定义如何计算这些存储。一个程序P定义一个标号转移系统。对于每个时刻t，对应于这样的转换系统的状态，该转换系统除了其他技术实体之外还包含经典项重写系统Ft。粗略地说，Ft的计算分四个阶段完成：P，P，P和P。我们在下面解释这些阶段。3.1过去的脚趾和过去的原子替换：PP是在时刻t由P通过消去脚趾和过去的原子而得到的。该演算由函数h：it执行，该函数取决于时刻t并且取决于定时重写规则的结构，使得在给定时刻t，P = hPit。出现在P中的形式为at（n s）的每个脚趾！被一个新的操作者B取代！其中，t0表示绝对instant的数量，即，在对应于at（ns）w.r.t.的时刻，Ref的值即时TBlanc，Echahed1020 的t0消去一个过去的原子，比如B，形式为3j1n1s1：：n2s2 j2 B0t0由表达式absinstant（n ;s;t）表示，并且满足以下性质：属性1在t0的那一刻，发生了一个滴答声。从时刻t0到t1，正好有n个s的滴答发生。因此，如果t是当前时刻，则abs instant（n;s;t）是在n tick s之前发生的时刻。函数abs instant是局部的。实 际 上，如果从第一时刻0到t 1发生了少于n个s的滴答，则不定义abs instant（n; s ; t）。如果一个过去的脚趾在（ns）！发生在定时重写规则中，并且未定义abs instant（n;s;t），则at（ns）！不能被评估，并且整个定时重写规则不会在P中发 生。通过扫描从t1back ards u n直到实例t0verifyingPro per ty1的过去的存储来执行绝对瞬时（n; s ; t）的计算。absinstant由以下规则正式定义：定义3.1（绝对瞬时）(i) abs instant（1 ;s; t）= t 1如果t > 0且F t1`！s == true(ii) abs instant（n;s; t）= abs instant（n1 ;s; t 1）如果定义了abs instant（n1;s;t1），则t > 0，n > 1且Ft 1`！s==true(iii) abs instant（n;s; t）= abs instant（n;s; t 1）如果ABS瞬时（n;s;t1）是定义的，t > 0，且F t 1`！s== false规则（i）停止了对过去存储的扫描，因为t 1验证了属性1。 规则（ii）和规则（iii）考虑到在前一时刻可能发生信号s的滴答继续扫描。通过对abs instant的第一个参数使用归纳法，可以直接证明absinstant（n; s ; t）验证性质1。当过去的脚趾是一般形式at（n 1s1）：at（n msm）！时，我们同样通过递归地迭代函数abs instant来进行，以获得对应于at（n 1s1）：at（n msm）的时刻。例3.2考虑图2。为了计算t 2，对应于at（n 1s1）at（n 2s2）w.r.t.我们需要rst来计算时刻t1。t1对应于关于时刻t的at（n1s1），即， t 1= absinstant（n 1; s1; t）。然后，从t 1获得t 2如下：t 2 = abs instant（n 2;s2;t 1）。在于用一个析取Wt02 j1t1;t2j2代替B hBi，其中t1=绝对瞬时（n1;s1; t）和t2= abs instant（n2;s2; t）。 如果未定义ABS即时（n 1; s1; t），则我们考虑t 1= 0。此外，如果abs instant不是在（n 2;s2; t）上定义的，则B被一个原子替换，标记为“0”，该原子总是为假。 如果析取是空的，那么我们认为B被替换为Blanc，Echahed10321t 2t11t1t1tn1 s1的时间点n2 s2的时间间隔Tickofs滴答声t2是对应于at（n1s1）at（n2s2）w.r. t的时刻。即时测试图二. 绝对瞬间to oo. 过去的例子--box原子，2j1n1s1.. n2s2j 2B0，类似于过去的钻石原子：析取变成合取，原子n2变成一个原子，记为TRUE，它总是为真。最后，下面给出h：it的形式定义。回想一下，P = hPit。通过滥用符号，我们注意到h：it在X上的应用，其中X可以是程序，定时重写规则，原子的结合，方程，项或脚趾。定义3.3（h：it）设P是一个程序，t是一个瞬间。 P = hPit定义如下。- 关于定时重写规则HPIt =F喜泰为2个PG- 关于定时重写规则hlhs ！tr=HSLHS（B）！HTR当Cithsit（hBIt当HCIt- 关于定时原子HB^ B0 It = HBIt --HB0 It- 在公式上沪1 ==u2It = 沪1It==胡二It- 在形式B = 2 j 1的过去盒原子上n 1s1：：n2s2 j2 B0Blanc，Echahed104hBi测试=Vt02j1 t1;t2j2hB0it0如果<8t1=绝对瞬时（n1;s1; t：t2=绝对瞬时（n2;s2; t））hBi不=Vt02[00;t2j2hBit0如果<8absinstantisnotdefined：t2=绝对瞬时（n2;s2; tintn=1;）S1; 不）hBit = 真如果absinstant未定义（n2;s2;t）- 在过去的金刚石原子上，形式为B =3j 1n 1s1：：n2s2 j2 B0Blanc，Echahed105hBi测试=Wt02j1t1;t2j2hB00it如果<8t1=绝对瞬时（n1;s1; t）：t2=绝对瞬时（n2;s2; t）HB我不0=Wt02[0;t2j2hB0It如果<8absinstantisnotdefined：t2=绝对瞬时（n2;s2; tintn=1;）S1 ; 不）hBit=0如果absinstant未定义（n2;s2; 不）- 按时间条件hxit = x（u1;：;um）it=喜泰 （胡1It;**;胡姆It ）- 戴在脚h！it=b！et如果！是非非时间性的Blanc，Echahed106h！it=！如果！是非时态帽子（n个S）it=hiabsinstant（n;S ;t ） 如果ABS瞬间被定义对（n;S; 不）在哪里！是一个定时算子，一个toe，s是一个信号，x是一个变量，lhs是一阶项，t rhs，u1; ： ;um1和umm定时项，B，B0和C定时原子，m 0，n > 0。例3.4考虑下面的玩具例子：1.f（x）！x+1当s> 15 == true2.f（x）！x-1当s 5 == true时3.m！ 当Ref ==0时为104.m！f（at（1s）m）当2 [-3Ref.. Ref] s10 == true，其中s：nat是输入信号，f：nat！ nat是一个定时操作符，m：nat是一个信号。假设s的滴答发生在时刻0，而不发生在时刻1。因此，在时刻2，该规格的P为：h1i2. bfe 2（x）！x+1，当 bs e2> 15 ==true h2 i2时。bfe 2（x）！x-1当 bse2 5 == true时h3i2。bme2！ 10，当bRefe2==0时h4i2. bme 2！bfe2（bme0）whenbs e0 10 == true^ bs e1 10 ==true在时刻0，P是：h1i0. bfe 0（x）！x+1当 bs e0> 15 == trueh2i0. bfe 0（x）！x-1当bse 0<5 ==trueh3i0时。bme0！ 10，当b参考e0==0时注意，h4i0在P中不成立，因为hat（1s）mi0未被定义。Blanc，Echahed1073.2添加需要的定义：P在第二阶段，我们计算一个新的程序P。其中In是定义输入信号的规则集，D由定义在P中引入的新操作符的重写规则组成，形式为b！0，其中0t0这样：Q是状态的集合。 一个状态是一对H ; F >，其中H，称为历史，是一个存储列表，F是一个存储。在P中出现的不同时刻的算子的存储。L是标签的集合，其中标签是定义传入信号的规则的集合。2即带参数3即可计算和终止Blanc，Echahed111！QLQ是如下定义的过渡关系。我们写在InC1！ 对于三重函数2！. 一个过渡！< [Ftj H];Ft+1>occursiFt+1是从程序P、历史[Ftj H]和由In给出的输入信号开始在instan t t + 1处计算的存储。Init是一个函数L！初始化的Q，使得如果In 0表示在时刻0的输入信号的定义，则Init（In 0）=<[]; F 0>。状态H ; F >由当前存储F和历史H组成，历史H是以前存储的列表。注意，F的计算可能需要一些我们可以在H中找到的旧存储的定义。4相关工作同步语言是专门为反应式编程设计的[10]。最具代表性的同步语言是Lustre[7]、Signal[9]和Esterel[2]。它们都是基于信号的概念，将程序编译成nite状态自动机。然而，这些语言不处理新的抽象数据类型或函数作为信号。因此，所需的泵功能不能像例2.2中那样直接定义此外，它们不提供强大的时态运算符，如时间间隔上的2和3。与我们的形式主义最接近的语言是声明性语言，即Lustre和Signal，其原语可以分为三类：经典的算术或逻辑运算符是扩展到流的静态运算符。我们可以把它们定义为非时态算子。延迟操作符（pre在Lustre中，$在Signal中）允许在执行期间访问信号的过去值。运算符包含这些运算符。多面体算子允许一个人表达来自具有不同时钟的其他人的新信号。这可以很容易地表示在我们的形式主义的尾部公式。至于Esterel，它更像是一种命令式的编程风格，并且，在我们的语义中，信号与Lustre和Signal不同。请注意，在我们的例子中，只要所考虑的应用程序不需要更有表现力的机器，就可以编译成nite自动机并发约束编程ccp[18]中时间概念的缺失导致了基于ccp并保持其良好特性的新同步范例tcc[16]的发展。 我们和tcc分享了一个非常有表现力的进化商店的原理。但是，商店变化的表达方式是完全不同的。在tcc中，悬挂物由进程生成，进程代数与悬挂物的形式表示公式正交。此外，这些公式是非时间性的，不重复。因此，从一个时刻到另一个时刻的数据传输是通过以下方式明确执行的：Blanc，Echahed112进程代数的下一个组合子。时间项重写系统是面向数据的，这意味着数据传输的机制对用户是隐藏的。tcc从ccp继承的一个问题是负面信息检测。在每个时刻，tcc可能只在存储计算结束时检测到信息的缺失，因此反应在一个时刻之后被放回。在[17]中提出了一个解决方案。新的范例被称为定时默认cc，能够检测到信息的缺失并立即做出反应。作为补偿，程序需要静态地进行验证以避免因果循环，而对于TCC程序则不需要（[16]的“无悖论”性质）。我们的商店是一个精心设计的战略，我ed重写系统，可以适应大范围的约束。一个布尔函数可以代表一个谓词，解决逻辑编程范式中的非问题，从而解决ccp的负信息问题。另一方面，ntcc[15]通过添加非确定性扩展了tcc。除其他外，这种模式有两个运营商注意到！然后呢？！P意味着\P在当前商店和未来商店中始终为真”，？P意味着\P在当前存储中或将来的某个存储中为真。 从逻辑的角度来看，！ 然后呢？是运营商2的未来的各自的代理商，3 .第三章。从程序的角度来看，！ 然后呢？可以被认为是一个生成器，而2和3是行为测试器。！然后呢？可以应用于未来的特定时间间隔。然而，该间隔使用基本时间单位表示：没有提供其他粒度。时态逻辑编程语言[14]也与我们的形式主义有关。Templog [1]和Gabbay的Temporal Prolog [8]等语言中的“temporal”的含义与同步世界中的含义不同。 时间实际上是在约束系统中表示的，并且在时间上不约束程序的执行。 所以，这种情况的因果关系在逻辑程序设计的这些扩展中，公式中的概念并没有被保留下来，而在我们的范例中却有。另一方面，这些语言有时态运算符2（总是）和3（最终），没有任何时间间隔的参考。Chronolog是一种数据流时态逻辑语言[19]，设计用于执行高效计算.但是，这种语言只管理一个时钟。由于对多粒度时间的需求在节奏编程中非常重要，因此开发了Chronolog（MC）[12]。然而，这种语言并不是同步的。5结论我们已经介绍了定时项重写系统作为一个保守的扩展经典的长期重写系统，允许一个人写声明性的程序，涉及时间。我们还精确地定义了这样的重写系统的行为，通过标记的过渡系统。这样的转换系统并不意味着定义实际的操作语义。我们在此引述两个主要原因：Blanc，Echahed113过渡系统状态的历史随时间而增加。因此，历史的实施是被禁止的。不同存储中的重写规则的大小也可以随时间增加。事实上，假设init是一 个 信 号 ， 它 的tick 只 发 生 在 时 刻 0 。 如 果 我 们 考虑过去的原 子B=2[1init：：1Ref]B0，则hBi3=hB0i0^hB0i1^hB0i2。 因此，合的长度在每一瞬间增加一。因此，包含该合取的某个定时重写规则的长度将以相同的速率增长对有效的操作语义学感兴趣的读者可以参考[3]。所提出的新语义允许人们处理现实世界的应用程序。主要的变化在于用有限的记忆集合代替历史。引用[1] M. Abadi和Z.吗哪时序逻辑编程。J. of Symbolic Computation，8（3）：277{295，September 1989.[2] G. Berry和G.贡蒂尔Esterel编程语言：设计，语义和实现。 计算机程序设计科学，19（2），1992。[3] Blanc和R.埃查赫德关于定时
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
