理论计算机科学电子笔记139（2005）145-168www.elsevier.com/locate/entcs基于π演算的Nepi语言中的名称传递风格GUI编程水野淳名古屋大学研究生院情报科学研究科，爱知县名古屋市筑草区不郎町1，邮编真野健2川边义信3NTT通信科学实验室，NTT公司，243-0198神奈川县厚木市若宫守里3-1Hiroaki Kuwabara4 Kiyoshi Agusa5名古屋大学研究生院情报科学研究科，爱知县名古屋市筑草区不郎町1，邮编袁宗二6名古屋大学研究生院情报科学研究科，爱知县名古屋市筑草区不郎町1，邮编JST PRESTO。邮编332-0012川口县本町4-1-81571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.001146A. Mizuno等人/理论计算机科学电子笔记139（2005）145摘要本文描述了在程序设计语言Nepi中的传名式图形用户界面（GUI）程序设计，Nepi的操作语义是基于π演算的重命名式传名通信。Nepi能够通过将等待前缀与外部选择相结合来实现定时行为。我们通过使用基于通道的行为特征化我们提出了一对扩展的语法元素'？g‘and‘！g '在Nepi中生成和终止图形组件。图形组件伴随着将事件转换为指定名称传递的在扩展的Nepi中，GUI程序被描述为实现实际功能的图形组件、事件处理过程和功能过程的组合。我们提出了一个Nepi的GUI扩展的实现编程语言Allegro Common Lisp，以示例说明Nepi中名称传递风格GUI编程最后，我们讨论了一个形式化的处理和验证技术的基础上扩展约简语义的Nepi。关键词：网络编程语言，图形用户界面，π演算，时间模型1介绍在构建交互式程序的图形用户界面（GUI）时，程序员描述GUI组件（如按钮和文本框）的图形外观和交互行为。由于这种编码遵循特定的模式，因此已经提出了许多GUI框架，例如KDE的Qt [4]，GNOME的GTK[2]和Java的SWING [9]。在许多GUI框架中，图形界面是通过组合GUI组件来构建的，其中所有的反应行为都作为“回调函数”嵌入到这些GUI组件中回调函数由关联的交互事件调用。回调函数的执行与程序的整个执行流程不同，因为回调函数通过来自环境的交互事件启动和终止。为了控制回调函数而嵌入代码来处理事件通常会导致元级编码，例如传递函数。在分析和理解GUI程序时，由于程序的状态难以识别，这种控制级别的不一致性往往会造成困难。本文提出了一种基于事件的GUI编程方法，该方法通过π演算中的名称传递来代替传统的函数式，即输入/输出、表征。我们的目标是提供一个基本的形式框架，用于分析交互行为和1电子邮件地址：a-mizuno@agusa.i.is.nagoya-u.ac.jp2电子邮件地址：mano@theory.brl.ntt.co.jp3电子邮件地址：kawabe@theory.brl.ntt.co.jp4电子邮件地址：kuwabara@agusa.i.is.nagoya-u.ac.jp5电子邮件地址：agusa@is.nagoya-u.ac.jp6电子邮件地址：yuen@is.nagoya-u.ac.jpA. Mizuno等人/理论计算机科学电子笔记139（2005）145147GUI组件GUI类名称界限（？于GUIgu（x）P）P{c/x}例如创建新鲜的名字(ofu类）CGUI环境Nepi图1.一、以名称传递方式处理GUI组件GUI程序。为了展示我们建模的真实效果，我们扩展了能够描述GUI程序交互行为的Nepi编程语言[7]。GUI程序被设计为图形组件和动作过程的组合图形组件和相关的事件处理进程从环境中捕获事件，然后传递相应的名称。动作进程调用与GUI相关联的相应动作。这种建模反映了GUI中基于事件的行为的本质，其中控制流由相关操作的事件传递名称传递风格的GUI建模简单描述如下。要创建GUI实例，需要将名称绑定到GUI组件。以名称传递方式处理GUI组件的基本思想如图1所示。扩展语法（？gu（x）P）创建一个GUI组件作为类u的实例。同时，它将一个新的名字绑定到x上，这个名字可以在P中自由出现。将名称绑定到GUI组件的实例，名称为启用接口的GUI功能，如打开/关闭操作和各种属性，如窗口大小参数的所有活动。为此目的，我们引入了一个粘结剂的语言除了ν-操作符。该名称通过接收一个特殊形式的对象名称，隐式地只与GUI环境通信。更多细节将在第3节中解释。Nepi语言直接描述了同步π演算的传名计算，包括定时行为。类似于CCS的选择操作符和等待前缀的组合启用了超时行为。我们将添加一对新的语法元素来为图形组件指定一个特定的名称。通过分配给图形组件的名称，事件被传递到调用函数进程中的方法，其中方法包装回调函数。由于Nepi语言采用Lisp S-表达式的名称表达式，我们扩展的语言绑定的Lisp图形包的图形组件的名称。我们在Allegro Common Lisp（简称ACL）和ACL通用图形包上实现了该扩展。我们提出了我们的Nepi语言扩展的设计和实现，148A. Mizuno等人/理论计算机科学电子笔记139（2005）145ACL，并通过提供一个典型的GUI示例来说明我们基于名称传递的GUI编程。为了享受Nepi语言的固有优势，即行为直接基于正式的名称传递模型，我们讨论了我们的扩展Nepi程序的正式操作语义。我们提出了抽象执行的Nepi程序的GUI扩展。我们讨论了验证技术应用于我们建模的方式。由于GUI环境在Nepi之外，并且Nepi以特定的方式通过ACL原语与GUI环境交互，因此我们给出了Nepi中GUI环境的描述通过将环境附加到Nepi GUI程序，GUI程序的执行通过标记转换来建模本文的组织结构如下。在第2节中，我们简要回顾了Nepi编程语言，第3节展示了GUI扩展的基本设计。在第4节中，我们介绍了扩展的Nepi语言。第5节详细介绍了实现机制，第6节提供了一些示例。第7节讨论了GUI函数的正式处理，第8节包括结论性评论和未来工作的简要介绍2Nepi编程语言：概述Nepi语言是基于π演算的通信过程模型设计的，用于描述TCP连接网络上的网络程序。 该语言的目的是在可靠的网络编程的帮助下，正式语义的名称传递演算。为了描述一个值表达式简化了对预定义数据的处理和对条件分支的控制，就像在其他流行的编程语言中一样。流前缀允许对文件等流数据进行延迟评估。该扩展使用LISP语法的效率的原因。下面是尼泊尔语语法的简要总结。更详细的解释见[5][6]。2.1值表达式一个值表达式是一个S-表达式，它的签名是关于常数C和变量V。C包括特殊符号{t，nil}和与h ' $ '相关的所有符号名CN。 你的眼睛在变. “的。 它包含了所有的Lisp内置函数和特殊的内置函数ch。ch将名称映射到真实的TCP端口。（chs1s2n）被评估为标识端口n上与s2指定的主机的TCP连接的名称，A. Mizuno等人/理论计算机科学电子笔记139（2005）145149进程表达式P：：=G保护的实验| (new ξ P)Name Creation| (par P1 P2)Concurrent Exec.| （ifu P1 P2）条件句| (a v1·· ·vn）进程调用| (? ew（x1x2）P） 开放流| (! e close（u）P）关闭流• 在上面的定义中，n≥ 0是一个数，u，v1，.。..，vn脸戒备G：：=end终止| (new ξ G)NameCreation| (+ G1 ·· ·Gn)Choice| (! u（v1·· ·vn）P）输出| (? u（x1·· ·xn）P）输入| （ifu G1G2）条件句| （bv1）·· ·vn）进程调用| （timen P）等待PG是是值表达式，w是Lisp对象，a∈n，b∈ndefproc-names，names是一个名称，x1，. ..，xn是不同的 变量。图二.尼泊尔语图三. Nepi的结构一致性s1的昵称。函数ch将一个名称映射到远程主机上进程的具体TCP通道。我们隐式地假设数据类型（如“integer”或“real”）LISP内置函数。2.2核心表达图2显示了核心流程表达式的语法 对于过程表达式P中的任意x ∈ V<$CN， 若 x 出 现 在 子 项 （ newx Q ） 的 下 划 线 部 分 ， 则（？ u（···x···）Q）或（？eu（···x···）Q），则x的这种出现称为有界的;否则，这种出现是自由的。虽然+在形式上是一个二元运算符（+P Q）。我们写（+G1. G n），由于运算符+的AC性质，具有任意数量的参数。我们在图3 -7中显示了结构一致性。的还原关系→对于图4中的核心表达式。当选择的分支是条件调用或进程调用时，该分支为7我们事实上，如果end是par的单位，则可以导出方程（+PQ）=（+（parPend）Q），这使得过程表达式类在结构同余下不封闭。150A. Mizuno等人/理论计算机科学电子笔记139（2005）145见图4。SOS尼泊尔语根据结构一致性规则进行简化例如，如果有一个过程定义（defproca（x1···xn）P（x1，.，xn）），过程表达式（+（av1···vn）Q）被简化为（+P（v1，.，v n）Q）。如果一个进程调用被defproc递归地定义为一个无保护的主体，如（defprocp p），那么该进程的行为可能会被定义为8。2.3扩展表达式在Nepi程序中，一个流通道可以像一个通常的名字一样被处理。 带有流通道的输入前缀绑定流的head对象，带有流通道的输出前缀将对象追加到溪 为了打开一个流w，我们写（？ew（x1x2）P）。 这会将新创建的流名称w绑定到x1，并将w的大小绑定到x2。例如，要打开一个文件/etc/hosts，我们写（？e'（（open“/etc/hosts”））（x 1 x 2）P）然后，为（file）流新创建的名称被绑定到x 1。x2绑定到一个新的名称，以获得一个控制信息，如文件大小。要关闭一个流，我们写（！eclose（u）P），其中流名称u被关闭，并释放用于该流的资源。这两个前缀都自动减少→。流前缀的进一步细节可以在[5][6]中找到在设计Nepi的过程中，引入流前缀来处理文件。它启发我们给出一个通用的语法来创建一个具有额外功能的名称。？e给出了一个文件流功能的名称。随后，我们提出了一个类似的绑定器，以给出GUI功能的名称。2.4时间行为为了描述时间行为，Nepi有一个时间前缀的形式：（timen P）这使得P在启动前等待n秒这里n可以是8.解释器可能试图无限扩展过程，导致无限循环。 但这只是一种反常的行为，与无限的还原序列不同A. Mizuno等人/理论计算机科学电子笔记139（2005）145151图五. 紧急求救任何值表达式。目前，为了按照预期的方式运行，n必须是一个值表达式，其计算结果为非负整数，在Nepi中称为“Number”。如果它的计算结果不是非负整数，则整个表达式将被计算为错误。图5显示了定时转换语义。 时间刻度是一个la beledbyy'1'. P→1PJ意味着一个单位时间后PevoPJ个通道好吗 由于时间前缀被归类为受保护的表达式，因此它使超时行为与选择运算符结合使用。 时间滴答P→1PJ使时间常数减小。当我到zero的时候，无声的过渡 请注意，这种无声的过渡解决了选择在那里实现超时选择。例如，（+（？chan（x）P）（time5Q））当它通过chan接收到一个名字时，表现得像P一样（用x的适当替换）。如果在chan上的5秒内没有通信，则它会减少到（+（？chan（x）P）（时间0Q））。 此时，如果chan上没有可用的通信，则通过在第二个被加数上进行选择，其行为就像Q丢弃第一个选择一样。基本的时间属性（直到结构同余）可以检查如下的时间确定性，最大进度和弱时间锁自由度[10]。时间确定性保持，因为没有关于定时约简的“动态”算子。最大的进步是-因为这是规则的前提条件弱时锁自由性成立，因为除了（时间0 P）之外没有紧急操作符。有可能通过无限还原锁定系统。3基于名字传递的我们将GUI组件建模为以下三种类型的通信过程的组成。(i) 图形组件：表示GUI组件（如按钮）外观的过程。它具有适当的属性，如大小或颜色。图形组件知道相关事件的名称152A. Mizuno等人/理论计算机科学电子笔记139（2005）145环境图形组件事件处理流程的创建事件发生的通知行动进程见图6。 GUI行为模型处理过程。环境通过传递名称来管理图形组件(ii) 行动过程：完成真正工作的过程。它对应于通常GUI编程中的回调函数。在从关联的事件处理流程接收到适当的名称后，它实际上对输入做出反应并与流程进行通信(iii) 事件处理进程：检测原始事件的发生并通过预先创建的名称传递发生通知的进程。假设图形组件在从动作流程发送请求时为每个事件创建事件处理流程。行为模型的概述见图6。除了上述三种类型的处理之外，假定存在控制图形环境的一个环境处理。环境进程接收来自动作进程的请求以启动图形组件。图形组件创建动作流程所需的事件处理流程。图形组件通过传递动作进程的名称来向所创建的事件处理进程通知动作进程。在这方面，使用了典型的名称传递功能。在这个初始过程完成之后，每次接受一个事件时，负责的事件处理流程都会将此信息发送给操作流程，然后对图形组件做出一些反应创建图形组件后，它会根据图形组件的属性创建事件处理进程。事件处理流程与真实环境中的原始事件（如按钮单击）进行交互，以获得相应的名称。关闭图形组件时，必须向组件发送特权名称以终止所有子组件。创建请求A. Mizuno等人/理论计算机科学电子笔记139（2005）1451534Nepi语言GUI扩展在本节中，我们将介绍Nepi语言中GUI建模的扩展语法及其行为。 我们引入一对语法元素？g和！G分别创建和终止图形组件。什么时候？g-prefix被减少，新创建的通道被绑定到图形组件。当！g-prefix with close被减少，图形组件被终止。4.1图形组件我们在图2中添加了以下前缀来操作图形组件：P：：=（？gu（gch）P）生成| (! g关闭（v）P） 终止其中u是定义图形组件外观的Lisp对象（通常由ACL Interface Builder生成），v是值表达式，gch是绑定到为图形组件创建的新名称的变量。注意到了吗？g-prefixes和！g-prefixes被归类为进程表达式，尽管它们的语法。 这是因为图形操作本质上不是用于控制行为的外部事件创建图形组件：（？gu（gch）P）从环境接收具有由u指定的外观的GUI通道c。用c代替gch在P中的自由出现。新创建的图形组件gc保持GUI通道c以与进程通信由于gch必须是“接地”的，因为所有的子组件都是初始化的，如果u具有未初始化的子组件，则对于每个子组件u j，（？guJ（gch）（！u（（listadd-graphic-componentuJ））end））是重新cursively创建，其中add-graphic-component消息添加uJ的图形子组件。图形组件的终止：（！gclose（v）P）评估值表达式v以具有GUI通道c，其中c=eval（v）。它通过一个众所周知的通道close向环境发送c，然后执行continationP。如果gc存在，则环境经由c向对应的图形组件gc发送终止信号。图形组件gc在接收到终止信号之后终止关 于 什么？g，对于每个子-具有GUI通道cJ的GC组件，（！g close（cJ）end）是递归的用于终止所有子组件。154A. Mizuno等人/理论计算机科学电子笔记139（2005）1454.2通过GUI通道一旦创建了图形组件，用户程序就可以向图形组件发送各种请求。格式为（！ gch（req_ret_ch）P）表示请求绑定到gch的图形组件的过程。这里req是一个列表，由一个请求指令和它的参数（可能没有参数）组成，ret-ch是用于将处理请求获得的值发送给操作过程 根据req的形式，绑定到gch是由指令操纵的获取属性值属性符号与图形组件的每个属性相关联。典型特性符号见表1。对于属性符号prop，列表（prop）是发送当前财产价值例如，（background-color）是对值背景颜色属性。 当图形组件接收到request（prop），它将属性prop的当前值发送给ret-ch。设置属性值设置属性值的请求是一个具有以下格式的列表：（：setprop v）。这里prop是一个属性符号，v是一个值表达式。当一个图形组件接收到这个请求时，它将属性prop的值更新为v，并通过ret-ch发送v。创建事件处理过程事件符号与每个事件相关联典型事件符号如表2所示。（：eventevent event-ch）是为事件创建事件处理进程的请求。如果一个图形组件接收到这个请求，它会尝试创建一个事件处理进程，如果成功则发送t，否则发送nil。每次事件发生时，创建的事件处理进程通过名称event-ch发送与事件有关的值。图形命令图形命令发送对图形组件本身的请求。典型的命令如表3所示（命令close仅供环境使用，而不供操作进程使用）。对由符号命令表示的命令的请求的形式为：（命令v1···vn）。4.3事件通知事件处理过程是通过向图形组件发送：event指令来创建的，用于捕获每个事件。 例如，一个prefix（！u（（list：event on-clickc）ret-ch）P） 创建一个事件处理过程，当原始事件“on-click”发生时，该过程准备在c上发送信号表4显示了原始事件和发送的值之间的对应关系A. Mizuno等人/理论计算机科学电子笔记139（2005）145155属性符号财产标题标题高度高度宽度宽度background-color背景颜色前景色前景色事件符号事件改变相关价值价值变动点击单击双击时双击鼠标进入时鼠标指针鼠标移出时鼠标指针表1图形组件表2图形组件命令符号命令论点返回值密切封闭图形组件没有一不设定键盘焦点获得键盘焦点没有一GUI通道添加图形组件采用图形组件GUI通道GUI通道诸如儿童儿童儿童表3图形组件事件符号值on-changeon-clickon-double-clickon-mouse-in鼠标移出时值单击图形组件双击图形组件鼠标按键下一个输入的指针，终止标记表4从事件处理流程发送的值通过返回通道返回。5执行根据Nepi语言的早期实现版本，GUI扩展使用ACL的通用图形包实现。本文通过一个实例简要介绍了使用通用图形软件包进行GUI编程的方法，并描述了与GUI相关的几个重要实现问题。156A. Mizuno等人/理论计算机科学电子笔记139（2005）1455.1ACL通用图形软件包在通用图形中，GUI组件（如窗口或按钮）被建模为一个具有属性和方法的称为小部件的对象。例如，（生成实例：top 100：left100：value：on-change nil：on-click nil）创建一个按钮小部件。top、left和value是对象的属性，100和OK是属性的值。 给定一个小部件wid和属性prop，由wid保存的prop的值通过计算（prop wid）获得。通过计算（setf（prop wid）val）将属性更新为val。对于每个小部件，可检测事件由公共图形定义，事件名称也被视为小部件的属性。给定一个带有可检测事件ev的小部件wid，通过将方法名称设置为ev，当ev出现在wid时，将调用该方法。5.2GUI功能至于整个Nepi系统，每个主机上运行一个Nepi处理器，主机通过TCP网络相互连接。当在主机上启动Nepi处理器，生成被动套接字。每个Nepi处理器都有一个名为地址的标识符，它是由IP地址和TCP端口号组成的一对。该地址用于与其他Nepi系统的通信和新名称的创建。随着Nepi系统的配置，每个名称都具有主机信息的属性，通道类型：REG（常规名称），STR（流数据通道），GUI（GUI通道）进程表达式保存在每个主机上的Nepi系统中称为进程环的内存区域中。系统从进程环中获得进程表达式，并将该表达式解释为要被约简。5.2.1图形组件操作创作：如果进程表达式（？gu（gch）P）在进程环中，一个窗口小部件wid并创建相应的GUI组件。通过本地主机上的Nepi新名称创建功能获得GUI的新通道结构对象。然后将一个三元组（c widnil）添加到图形组件表中，最后gchisP的每个自由出现都被c替换，其中nil是用于处理事件的初始空列表A. Mizuno等人/理论计算机科学电子笔记139（2005）145157终止日期：让进程表达式为（！g关闭（u）P）。存在两种情况，取决于通过评估u获得的通道c。如果c是本地主机上的一个通道，则系统在图形组件表中搜索具体窗口对象和事件处理列表。在向c发送关闭信号之前，该过程通过发出！g-前缀（续）到工艺环的末端。如果c是远程主机上的通道，本地Nepi处理器会发出一个进程表达式（！g靠近（c）端）到远程系统的处理环。5.2.2处理请求对GUI组件的请求是通过减少前缀来处理的，前缀的主题是由？g-预置。注意，前缀作为受保护进程表达式的第一个元素出现。虽然选择运算符+的抽象语义遵循常规选择，但Nepi系统尝试从左到右的守卫，因为与实现有关的实际原因。（具体实施机制见[3]）你好啊，我是说，我是说， ch（reqret-ch）Pi）是选择的。 当nch被评估为本地名称c时，Nepi处理器通过在图形组件表中查找来向图形对象发送对c的请求。 如果CH是作为远程主机上的名称进行评估，本地Nepi处理器将（啊！CH（REQRET-CH）结束）。获取和设置属性值属性值是通过将通道转换为相应的窗口对象来获取或设置的，在图形组件表中查找。例如，（！如果三元组（ch_win_alist）存在于表中，则ch（（list_title）ret）P）发送对应于ch的图形对象win。属性值由setfLisp宏设置。如果发生任何错误，ret会返回一个特殊的值err。创建事件处理流程假设req是创建事件处理流程的请求，即（：eventev ev-ch）是通过对req求事件符号ev和名称ev-ch而得到的。然后系统计算（setf（ev wid）func ev）。使用公共图形事件工具，当wid的事件ev发生时，函数funcev被调用。这样的函数funcev在Nepi系统中为每个ev定义。图形命令如果req是一个执行命令的请求，Nepi处理器只需要将相应的窗口作为第一个参数执行命令;（command wid v1···vn）。158A. Mizuno等人/理论计算机科学电子笔记139（2005）145需要注意的是，处理4.1中提到的图形子组件是作为命令请求实现的（！ gch1（（listadd-graphic-componentgch2）ret-ch）end）系统评估（listadd-graphic-componentgch2）并获得列表（add-graphic-componentgch2）。然后，它在对应表中查找一个条目（gch1wid1alist1），并计算表达式（添加图形组件wid1gch2）使用Nepi提供的函数add-graphic-component。结果，与GUI通道gch2对应的控件被添加到wid1的子控件列表。5.3事件通知如上所述，当对于窗口小部件wid发生在创建事件处理过程时登记的事件ev时，评估表达式（funcev wid v1···vn）。这里，v1，。。.是与事件相关联的值。函数funcev试图找到一个形式为（ch wid alist）的三元组。假设（ev. ev-ch） 是alist中汽车部件为ev的第一个元素。然后（！ev-ch（v1···vnnil）end）添加到工艺环中。除了关闭！g，如果wid是一个窗口，则可以通过单击标题栏上的“x” 按 钮 关 闭 wid 。 在 这 种 情 况 下 ， （ closewid ） 会 被 CommonGraphics自动求值，这会导致调用上面描述的close6例如我们提出了一个文件复制器，复制一个文件到另一个与进度条。首先，程序在屏幕上显示主窗口（图7）。此窗口有一个开始按钮和两个输入表单。当按下开始按钮时，程序创建一个进度条窗口（图8），并开始复制文件的过程。此程序仅在以下情况下终止：（i）文件传输完成;（ii）用户单击进度条窗口上的取消按钮;或（iii）开始按钮未被触摸60秒。A. Mizuno等人/理论计算机科学电子笔记139（2005）145159文本标签文本标签进度条按钮见图8。进度条窗口见图7。主窗口6.1用ACL在图形组件的设计上，我们使用了ACL的GUI生成器IDE。 IDE有一个用于设计窗口的图形编辑器，它会生成相应的S表达式。在文件复制器示例中，IDE为主窗口生成一个Lisp程序是一个Lisp程序也产生了dow。当值表达式（make-copy）被评估时，Nepi系统在屏幕上 显 示 主 窗 口 ， 并 返 回 一个“wid g e t 0” 的 小 窗 口 。然 后 ， 将 值（widget1· · ·widget5）设置为小部件0的属性“dialog-items”，其中图7中的每个GUI组件具有数字i ∈ { 1，. .，5}，其对应于小部件i。程序员可以在形式（？）的下划线部分使用表达式（make-copy）。g（make-copy）（gch0gch1···gch5）P）。请注意，我们可以编写六个GUI通道gch0，. ，gch5在这个形式，这意味着这个形式是一个扩展的？g-表达式。 这种扩展形式是通过创建新的名称gch1，. 、gch5并将它们分配给窗口小部件窗口小部件1、. ，widget5，re-- 是的6.2文件复印机图9是文件复印机的程序代码这个程序有四个进程定义• 顶层进程nepicopy显示主窗口。这个过程向开始按钮的GUI通道发送一条消息（：eventon-change$start-ch）• 进程启动处理程序是主窗口的一个动作进程。当按下主窗口上的开始按钮时，此过程执行以下操作。首先，start-handler从主窗口上的两个输入表单中读取文件名，并使用它们替换变量文本标签输入表单（用于输入文件）输入表单（用于输出文件）按钮按钮文本标签160A. Mizuno等人/理论计算机科学电子笔记139（2005）145和“.to-file”。然后，这个过程试图打开文件。 当出现故障时，该过程将显示一个弹出窗口，提供通知的失败。打开这些文件后，该过程创建一个进度条窗口，并为进度条窗口的取消按钮生成一个事件处理过程此过程在60秒内超时如果没有事件.start-ch发生时，它关闭窗口，并且其子组件死亡。• 进 程copy-handler是 进度 条 窗口 的 动作 进 程;copy-handler 1是copy-handler的子例程。此进程由start-handler调用，并尝试执行以下两个操作之一：· 第一个动作是从cancel按钮的事件中接收消息通过名称“.cancel-ch”处理进程如果消息包含变量“.fin”的值t否则，进程将关闭进度条窗口;· 第二个动作是从流通道“.input”中读取一行 如果线是“0”，则进度条窗口关闭。否则，该过程将该行附加到输出文件，然后附加一些属性值在进度条窗口中进行更改7讨论本节讨论Nepi程序中GUI行为的形式化操作语义。我们定义了一个基本的过渡系统，考虑到在计算过程中创建和销毁的图形对象。7.1GUI行为我们假设为小部件保留一组通道Gch。具有Gch的一些名称的封闭进程表达式被称为GUI系统。定义7.1图形上下文以如下方式递归给出：• []是图形上下文;• 当G是图形上下文时，u是图形上下文;并且• vv. G，其中v是一个名字，u∈Gch。当[]被G中的一个过程表达式P代替时，我们写G[P]。 G中的一组自由名fn（G）定义如下：fn（[]）=n; fn（G，nv：uv）=fn（G）n {v}; fn（v v v）。[1][2][3][4][5][6][7][8][9][10][11][12][12][13][14][15][16][17][18][19][ 19Nepi操作语义[6]扩展为图形标签，如图10所示。与GUI操作相关的转换由Gch标记以反映效果A. Mizuno等人/理论计算机科学电子笔记139（2005）145161Gg0克1 1克2 2克αG的图形外观。直觉上，G[P]表示G的图形外观中的动作过程P。 过渡到？g在G中创建了更多的图形对象，并且！g在G中终止图形对象。GUBehvior是r→α的跃迁如图11所示。G[P]→GGJ[PJ]表示过程P具有G通过α的影响，随着GJ的更新的图形外观而演变为PJ。GUI系统的执行从空的图形上下文开始由f→τ改变图形特性的序列产生。虽然G不直接保存屏幕图像，我们记录的是图形对象的类型我们认为一个执行程序可以保存足够的信息来区分图形外观。定义7.2给定一个GUI系统P，P的执行是f→τ的（可能无限）s序列→1用P.P=P→αG[P]→αG[P]→α· · ·其中α是τ或1。在执行中，只有τ或1可能出现在过渡中。P的形式为（parU Env），其中U是用户程序，Env是所有用户程序所共有的环境。用户程序U在环境Env下操作。在上面的形式化中，Env必须包括与外部交互的所有模式，以便表示完整的执行集。这样的环境是无法表达的一般的纯过程表达形式。在Lisp内置函数的帮助下，我们可以获得完整环境的合理近似值，如下一节所示。7.2该环境描述而从更具体的角度对GUI程序的行为进行建模，我们使用Lisp内置函数在Nepi语言中显示环境G162A. Mizuno等人/理论计算机科学电子笔记139（2005）145（defproc Env（）（new$open-ch(par（close-gc nil $open-ch）（GEnvexp-1$open-ch）（GEnvexp-2$open-ch）... ）））（defproc GEnvu（.open-ch）（new $gch（！.open-ch（$gch）（！u（$gch）(par（NewGraphicComponentu$gch）（GEnvu.open-ch））（defproc close-gc（.open-lst .open-ch）（+（？close（.close）(if（member.close.open-lst）（！.close（（listclose））（close-gc .open-lst））（close-gc .open-lst.open-ch））（？ .open-ch（.open）（close-gc（cons .open .open-lst）.open-ch）这里是exp-1，exp-2，. 是表示图形组件的所有表达式的序列。虽然这种求和一般可以是无限的，但给定一个用户程序，程序中出现的类的集合是固定的。生成u实例的进程被定义为进程GEnvu由u参数化。 进程GEnvu创建新的GUI通道$gch，将其发送到close-gc。在通过u发出$gch时，进程启动相应的图形组件（NewGraphicComponentu$gch）。 处理关闭请求的进程以close-gc的形式给出。该过程在列表.open-lst中累积通过.open接收的图形组件的名称。在接收到关闭请求时，流程将其转发到相应的图形组件，并从.open-lst中删除名称。上面的环境描述让人想起Walker在π演算[11]中的对象描述，其中实例创建被建模为传递私有名称以调用实例。由于Nepi没有复制操作符，我们用defproc递归编写它。7.3行为属性如前所述，为了在Nepi中验证用户GUI程序，我们必须将程序置于环境中以检查其执行情况。上一节中的环境描述提供了合理的A. Mizuno等人/理论计算机科学电子笔记139（2005）145163与Nepi实现相关的给定用户程序的对应物。由于与外部的交互模式不是完全特定的，我们无法验证GUI程序的行为。然而，通过限制交互模式，可以验证关于交互模式的属性。例如，图形组件（defproc进程-窗口（.gch .progress .cancel .val .text）（？.gch（reqret-ch）(if（eq（firstreq）close）（！.progress（（listclose））（！.cancel（（listclose））（！.val（（listclose））（！.text（（list close））end）（-window.gch .progress .cancel.val.text）在第6节中指定进度条。该图形组件通过GUI通道“.gch”接收命令“关闭”，并通过通道“.progress”、“.cancel”然后，图形组件终止。类似地，构成GUI系统的其他进程可以在Nepi中描述。通过检查程序的执行情况，我们可以讨论程序的性质。例如，下面的属性应该适用于第6节中的程序：属性：在按下开始按钮后，如果按下进度条窗口上的取消按钮，则窗口将最终关闭。这个属性可以重述为所有的执行都以空的图形上下文终止。根据复制功能和取消之间的竞争，即使按下取消按钮，窗口也可能在复制结束时关闭。为了证明这个属性，我们只需要考虑正则表达式中事件模式的有限环境“（从|To）Start. （进展情况）|文本|Val）取消’这样的环境可以用有限的方式来表达。我们还没有开发出任何具体的技术。我们期望通过将环境表示为待执行的实验和公共环境的组合来具体化此类有限环境。在这个意义上，上述讨论的为了直接验证行为属性，有必要将整个环境纳入Nepi，使行为在系统内得到完全控制。理论上这应该是可能的，但在实际意义上，由于Nepi旨在提供与ACL相结合的高级描述，因此我们认为在此级别检查属性很可能是164A. Mizuno等人/理论计算机科学电子笔记139（2005）145Nepi程序的验证。7.4相关工作Nomadic Pict[13]是一个基于π演算的编程系统。它可以处理ObjectiveCaml的图形库[12]。在对No- madic Pict的建模中，名称表示用于基本操作的接口，例如绘制线或圆、打开屏幕或检测鼠标单击。例如，为了画一条线，两端的位置通过一个名称“lineto”发送游牧的皮克特GUI库没有小部件，因此程序员应编写代码为他/她自己的小部件。相比之下，通过为图形组件分配名称，我们可以在Nepi中使用Common Graphics的小部件并发ML[8]是标准ML的并发扩展，它以与Nepi相同的方式提供同步通信，名称创建和非确定性选择它有一个名为eXene的GUI库[1]，其中包含并发ML中描述的各种然而，eXene的建模强烈依赖于X窗口系统的渲染模型和事件路由实现[14]。另一方面，Nepi因此，我们希望这种方法是成功的其他面向对象的GUI系统。8总结发言我们在Nepi编程中通过扩展一对前缀提出了名称传递风格的GUI编程？G和！G.我们在Allegro Common Lisp上扩展了Nepi语言处理器。在名称传递风格中，GUI程序由图形组件和动作进程组成图形组合事件接受外部事件，例如单击按钮以发出要传递给操作进程的名称。GUI程序的行为被建模为基于Nepi语言的操作语义的转换系统[5]。 在我们的模型中，没有必要纳入高阶设置中使用的传统功能治疗。通过观察这两类组件之间的通信，我们可以抽象出图形组件的详细信息。因此，当仅在图形组件中发生改变时，不需要修改动作过程。这有助于GUI编程的可移植性。的介绍？G和！g表达式是Nepi的扩展，？g为图形组件分配唯一的名称，并且！g关闭一个图形组件，以便显示相关的操作过程和图形。
