98理论计算机科学电子笔记66第三次（2002年）网址：http://www.elsevier.nl/locate/entcs/volume66.html18页“环境感知”计算的演算费鲁西奥·达米亚尼2意大利都灵信息技术大学Paola Giannini2Dipartimento diInformaticaUniversit`adelPiemonteOrientale Alessandria，Italy摘要我们提出了一个演算建模的“环境感知”的计算，即计算，适应自己的行为，根据能力的环境。演算是一种命令式的、基于对象的语言，具有可扩展的对象，配备了标记的转换语义。互模拟的概念，提升计算之间的对应关系的能力不同的环境，提供。互模拟可以用来证明程序是“跨环境”的，即，当在不同的环境中运行时，它具有相同的性能。1介绍基于移动代码的分布式计算代表了现代软件系统的一个重要在开放广域网的概念模型中，资源在网络上共享和分布，代码迁移到不同的环境中执行，即在不同的环境中执行在不同的地理或日志位置，访问不同的系统资源并依赖于不同的系统服务。软件系统通常使用静态类型的编程语言来实现。 静态类型操作器支持的可靠性和维护1由IST-2001-33477 DART和MURST Co fin'01 NAPOLI项目部分支持2电邮地址：{bono，damiani，giannini}@ di.unito.it2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。波诺，达米亚尼和吉安尼尼99软件然而，它对代码的适应性施加了限制特别地，软件配置在严格地在运行时之前发生的编译时执行脚本语言，参见[12]，主要用于将组件在一起，而不是从头开始构建系统例如，Tcl [11]和Visual Basic [6]可以通过在屏幕上排列用户界面控件的集合来生成用户界面为了方便连接不同组件的工作，脚本语言是无类型的，允许变量引用不同类型的对象。代码和数据是可以互换的，允许在编译器上产生的代码执行;为此，这些语言通常是解释的，而不是编译的。互联网的发展使脚本语言流行特别是JavaScript（参见[9]），它已成为流行的Web页面脚本。JavaScript是一种强大的基于对象的语言，可以直接嵌入到HTML页面中。它允许创建在Web浏览器中完全运行的动态交互式应用程序。JavaScript是一种基于对象的语言（参见[1，8]），具有可扩展对象（参见[7，2，3]）：修改尚未定义的属性会导致该属性的定义。尝试读取不存在的属性的值会导致特殊的未定义值。通过这种方式，解释器可以检测对象和属性的存在，并尽可能地继续下去。[3]有趣的是，依靠这些特性，一些技术已经被开发出来，用脚本代码来编写Web页面，这些脚本代码可以根据它们运行的浏览器来调整它们的行为（参见[13]）。在DART项目[5]中，我们正在解决动态重新配置软件片段的问题，一方面，我们研究如何为静态类型语言添加可扩展性，另一方面，我们研究可能表现出脚本语言的可扩展性的基础演算。在本文中，我们提出了一个演算做一些推理的性质，如JavaScript语言编写的程序我们提供了一个标记的过渡语义的一个命令式的基于对象的语言中，对象是可扩展的，它是可能的，以测试环境中的对象的属性的存在，并提出了一个概念的互模拟，占在不同的环境中的程序在这个框架中，我们可以证明一些程序是跨环境的，即，它们在不同的环境中运行时具有相同的行为。本文件的结构如下。 在第2节中，我们通过一个例子介绍了该框架。在第3节中，我们提出了语法和操作语义的语言。在第4节中，我们定义了互模拟。我们的结论是，3这与“Web哲学”是一致的程序员不是专家。然而，它使得JavaScript不太适合以更传统的方式编程，而是使用静态类型编程语言。波诺，达米亚尼和吉安尼尼100E根
图1：环境E概述了进一步工作的一些方向在附录A中，我们提出了一个案例研究：我们使用我们的框架来证明动态HTML页面（包含JavaScript代码）是“跨浏览器 ” 的 在 浏 览 器 IE5 （ Internet Explorer 版 本 5 ） 和 NN4 （ NetscapeNavigator版本4）中运行时具有相同的行为2建立框架该文件所制定的框架按以下定义描述• 环境=一组对象。• Language=一种基于对象的命令式语言，· 扩展对象，以及· 区分对象属性的存在/不存在• 可观察行为=环境中对象的某些属性的变化对象有字段和无参数方法。方法的接收者是方法的隐式参数，可以通过元变量self来寻址。对于每个环境E，存在顶层对象。当在环境E中执行表达式e时，关键字root被绑定到E的顶层对象。在本节中，我们将通过一个简单的例子介绍框架中使用的基本思想：屏幕上的彩色点。着色点由x坐标、y坐标和颜色确定。图1中的环境包含位于坐标（4，8）处的黑点的表示：顶层对象的属性cp指的是表示着色点的对象通过观察集合中属性的值（的变化）来监视着色点的状态（的变化）P ={root. CP. x，根。CP. y，根。CP. c}。着色点的另一种表示由环境提供EJ，其中观察到的属性集是PJ={root. cpoint。点xcoord，root. cpoint。点ycoord，根。cpoint。color}。现在考虑编写一个程序的问题，该程序通过交换着色点的x坐标和y坐标来修改着色点的状态。的>波诺，达米亚尼和吉安尼尼101EEE根表达式：图2：环境EJe = root←t= root 。 CP. x;（1）根。cp←x = root。CP. y;（2） r oo t. cp←y=r oo t。不（三）在环境中执行此任务。具体地说，（1）将新属性t添加到顶层对象，并为其分配x坐标的值(2)将y坐标的值赋给x坐标，以及（3）将属性t的值在y坐标上。表达eJ= root ← t = root. cpoint。点xcoord;root. cpoint。point←xcoord = root. cpoint。点ycoord; r oo t.克蓬湾点←ycoord=r oo t。不在环境EJ中执行相同的任务。通过观察环境E中的P中的属性的值（的变化）和环境EJ中的属性Pj的值（的变化）来监视着色点的状态（的变化）的观察者不能区分E中的e和EJ中的EJ的行为。本文提出了互模拟的概念，它可以表示，模P中列出的E的属性和PJ中列出的EJ的属性之间的对应关系，R={（root. CP. x，根。cpoint。点xcoord），（根。CP. y，根。cpoint。点ycoord），（根。CP. c，根。cpoint。color）}P×PJ，e在中的行为等价于（R-双相似）eJ在中的行为。J.此外，互模拟的概念可以用来表达程序属性，如下所示。• 表达e0=isdef（root，cp）？e：EJ，(that在顶级对象具有属性cp的环境中表现得像e，否则表现得像eJ），在两者中具有相同的行为>波诺，达米亚尼和吉安尼尼102E∈∈⟨⟩e∈Exp：：= n|e1ope2|e1; e2|e0？e1：e2|根|自我|⟨ ⟩ |e.a |isdef（e，a）|e1← a = e2|e1a = e2图3：表达式E和EJ。• 在环境中，表达式e具有表达式eJJ=r oo t。cp交换=（self←t=sel f. x;self←x=sel f. y;self←y=sel f. t）;root. CP. 交换它首先将swap方法（交换接收器的坐标）添加到表示着色点的对象，然后调用它。3微积分在本节中，我们将介绍允许定义和操作对象的核心语言的语法和操作语义3.1语法该语言对应于JavaScript的核心部分[9]。唯一考虑的表达式的句法类别，由图中的语法3，是参数在一个无限集的属性名称A。前两个子句定义整数表达式（整数字面量的nN范围和整数上的二进制操作的op范围）。序列组成的表达式，E1;E2，是从左到右评估，其值是E2的值。条件表达式，e0？e1：e2，通过第一次求值e0进行求值，然后是e1（当e0求值为不同于0的整数时）或e2（当e0求值为0时）。当e不返回整数时会发生错误。表达式root表示环境的顶级对象self是一个元变量，表示方法执行期间的当前对象（在方法体之外，其值没有定义，其求值会产生错误）。表达式是空对象，e. a是从表达式e表示的对象中选择属性a。如果一个绑定到一个值（要么是一个整数，要么是一个对象的地址），则返回该值。如果一个绑定到一个方法体（一个非求值表达式），那么这个方法体将被求值。当e不表示对象或所表示的对象不具有属性a时，会发生错误。如果e表示的对象具有属性a，则表达式isdef（e，a）的计算结果为1，否则为0（当e不表示对象时发生错误isdef的预期用途是结合条件来编程环境相关行为。波诺，达米亚尼和吉安尼尼103∆⟨⟩∆·表达式e1←a=e2是对一个对象的属性的覆盖或添加，这取决于这样一个事实，即对于由e1表示的对象，属性a是否被定义属性a被设置为从e2的评估得到的值。类似地，表达式e1a=e2将属性a设置为由（未求值的）表达式e2表示的方法体，其中元变量self已被由e1表示的对象的地址替换。在e2中，符号“自我”的出现与“自我”绑定。3.2操作语义我们定义了一个标记的转换语义（参见例如，[10]），其中标签表示属性的添加/重写。语义以[14]中主张的风格呈现（另见[4]）。表达式的计算结果可以是整数或对象的地址。环境将地址映射到对象。为了说明语言的命令性质，标记转换系统除了重写表达式外，还重写语义由一个归约关系定义−→（Env×EExp）×Lab×（（Env×EExp）+{err}），根据另一个归约关系定义− →（Env×Red）×Lab×（（Env×EExp）+{err}）和评估上下文（见图5）。特殊术语err用于模拟运行时错误。定义−→所涉及的语义范畴是：• 扩展表达式，e∈EExp，通过添加子句“|i“到语法定义表达式（见图。3），其中i∈I是地址。• 值，v∈ValEExp：：= n|ι• 对象，o ∈ O = A →finEExp，即， 从属性名到扩展表达式的有限映射，表示为a1= e1，...，an= en。给定一个对象o，设o[a：e]表示对象，使得o[a：e]（a）=e和o[a：e]（aJ）=o（aJ），其中aJ/=a。• 环 境 ， E ∈Env = I→finO ， 即 ， 从 地 址 到 对 象 的 有 限 映 射 ， 用 [i1<$→o1，.，n→on]。对于每个环境E，都有一个地址iroot（E）（E中顶层对象的地址），使得E（iroot（E））/= UNDEFINED。令E[i：o]表示环境，使得E[i：o]（i）=o且E[i：o]（iJ）=E（o），其中iJ/=i。∆• Labels，Lab = · |！a，其中i！a意味着，地址1处的对象已经被添加/覆盖，并且意味着没有属性被添加/覆盖。• 赎回权e ∈ RedEExp：：=n1op n2|v;e|n？e1：e2| 根|自我|⟨ ⟩ |i .a |isdef（i，a）|i ← a = v |a = e波诺，达米亚尼和吉安尼尼104E× ×∈E EEE/E实验室实验室• 评价背景，EC ∈ C：：= [ ] | EC;e|EC？|EC? e1：e2| EC.a |isdef（EC，a）|EC ← a=e|i ← a=EC|ECa=e对于整数op上的每一个二元运算，都有一个三元关系op=N N N使得：（n1，n2，n）op当且仅当n是n1op n2的值。 在扩展表达式e中，自性的自由出现被地址i，e[i/self]所取代，由Fig.中的子句定义。四、标记的转换系统重写成对（，e）的配置，其中e是扩展表达式。一个扩展表达式e是封闭的，如果它不包含self的自由出现，一个环境是封闭的，如果它不包含self的自由出现，并且对于所有i出现在中，（i）= UNDEFINED，一个配置（，e）是封闭的，如果和e都是封闭的。我们对封闭环境中封闭表达式的执行图的归约规则五是自我解释。只需要注意在规则（att）中，元变量self在e中被替换为方法所添加到的对象的地址关系−→和−→是确定性的（由规则（OBJ）引入的对地址的模重命名），并享有进展属性，如以下引理所述。引理3.1（−→的进展）如果（E，e）∈Env×Red，则• 或者（E，e）−→（EJ，eJ），对于某个标签实验室和配置（EJ，eJ），当（E，e）是闭的时，• 或（E，e）−→·err.引理3.2（唯一分解）如果e∈EExp，则• 或者e∈Val，• 或者存在唯一的EC ∈ C和EJ∈ Red使得e = EC [EJ]。引理3.3（−→的进展）如果（E，e）∈Env×EExp，则• 或者（E，e）−→（EJ，eJ），对于某个标签实验室和配置（EJ，eJ），当（E，e）是闭的时，• 或（E，e）−→·err.例3.4图6中的-→-归约表示在图6的环境E中执行第2节末尾给出的表达式EJJ1.一、4互模拟的概念在本节中，我们提出了互模拟的概念，提升到计算不同环境的可观察属性之间的对应关系。波诺，达米亚尼和吉安尼尼105self[i/self] =ie[i/self]=e，如果e∈N<$I<${根，根}（e1ope2）[i/self]=e1[i/self]ope2[i/self]（e1;e2）[i/self]=e1[i/self];e2[i/self]（e0？e1：e2）[i/self]=e0[i/self]？e1 [i/self]：e2[i/self]（e.a）[i/self] = e [i/self].a（isdef（e，a））[i/self]=isdef（e[i/self]，a）（e1<$a=e2）[i/self]=e1[i/self]<$a=e2[i/self]（e1a=e2）[i/self] =e1[i/self]a=e2图4：操作语义：替换e[i/self]（OP） （E，n1opn2）−→·（E，n）with（n1，n2，n）∈op（SEq） （E，v;e）−→·（E，e）（I FT RU E）（E，n？e1：e2）−→·（E，e1）其中hn/=0（I FFALSE） （E，0？e1：e2）−→·（E，e2）（OBJroot） （E，root）−→·（OBJ）（E，）−→·（ATT。） （E，I.a）−→·（E，iroot（E））（E[i：]，i）与i新鲜（E，e），其中E（i）=o且o（a）=e·0，如果O（a）被定义为（ATTisdef）（E，isdef（i，a））−→（E，n）其中E（i）=o且n=01、否则（ATT←） （E， i←a=v）−i！→a（E[i：o[a：v]]，i），其中E（i）=o（ATt）（E， ιa=e）−ι！→a（E[i：o[a：e[i/self]，i），其中E（i）=o（ERR） （E，e）−→·err，如果e不是一个值，并且没有前面的规则可以应用（CNT）（E，e）−la→b（EJ，eJ）（CNTERR）（E，e）−→·err（E，EC[e]）−la→b（EJ，EC[eJ]）（E，EC[e]）−→·err图5.操作语义：−→和−→归约规则波诺，达米亚尼和吉安尼尼106← ←←⟨⟩（E，eJJ） −→·−→·我来！交换（E，iroot（E）. cpswap = eswap; root. CP.swap）（E，ιcpswap = eswap; root. CP. 互换）JJ−→（E1，ιcp; root. CP. 互换）−→·−→·−→·−→·−→·我来！不（E1J J，r oo t .）CP。swa p）（E1J J，iroot（E）. C P。swap）（E1J J，icp. swap）（E1J J，eJswap）（E1J J，icp<$t=4;icp<$x=icp。y;icp←y=icp。t）的范围内JJ−→（E2，Icp;Icp←x=Icp. y;icp←y=icp。t）的范围内−→·−→·我来！X（E2J J，Icp←x=Icp. y;icp←y=icp。t）（E2J J，icp<$x=8;icp<$y=icp. t）的范围内JJ−→（E3，Icp;Icp<$y=Icp. t）的范围内−→·−→·我来！y（E3J J，Icp←y=Icp.t）（E3JJ，ιcp←y=4）JJ其中：−→（E4，ιcp）• eJJ=（root. cpswap = eswap; root. CP. 交换），与eswap=（selft=sel f. x;selfx=sel f. y=self. t）是第2节末尾给出的表达式。• E= [iroot（E）<$→oroot，icp<$→ocp]，其中oroot= icp=icp是顶层对象，以及ocp= x = 4，y = 8，c = 0表示着色点的对象是图1中的环境。• E1JJ=[iroot（E）<$→oroot，icp<$→oJcp]，其中oJcp=0，x=4，y=8，c=0，swap=eJswap0，以及eJswap=eswap[icp/sel f]=（icp←t=icp. x;Icp←x=Icp。y;icp←y=icp。t）。• E2JJ=[iroot（E）<$→oroot，icp<$→oJcJp]，其中oJcJp=0x=4，y=8，c=0，swap=eJswap，t=4 x.• E3JJ=[<$root（E）<$→oroot，<$cp<$→oJcJpJ]，其中oJcJpJ =x = 8，y = 8，c = 0，swap = eJswap，t = 4。• E4JJ=[<$root（E）<$→oroot，<$cp<$→oJcJpJJ]，其中oJcJpJJ=x=8，y=4，c=0，swap=eJswap，t=4。图6：在E中执行eJJ波诺，达米亚尼和吉安尼尼107EEE{}E E--E4.1可观测属性路径，由以下语法定义：p：：= root|p. a，形式化给定环境的可观察属性的概念。由环境中的路径p表示的扩展表达式eexpE（p）定义为：eexpE（root）=iroot（E）如果eexp（p）=i，（i）=o，且o（a）=e，则为eexpE（p.a）=100未定义，否则。可以通过覆盖/添加路径p中出现的属性（actE（p））来改变E中由p表示的扩展表达式的标签集合由下式给出：actE（root）=0act（p）ι！a，如果eexp（p）= iactE（p.a）=行为E（p），否则对于每一个路径集P，定义actE（P）=P∈PactE（p）。命题4.1如果（E，e）−1！→a（EJ，eJ），则对于每个路径p，(i) ！a∈actE（p）当且仅当！a∈actEJ（p），以及(ii) ！a/∈ actE（p）意味着actE（p）= actEJ（p）和eexpE（p）= eexpEJ（p）。例4.2对于图4的环境 6（也参见图1中的图形表示）和路径集合P = root。CP. x，根。CP. y，根。CP. c在第2节开始时介绍，我们有：eexpE（root. CP. x）=4，eexpE（root. CP. y）=8，eexpE（root. CP. c）=0，ac tE（P）={root（E）！ c p，icp！ x，icp！ y，icp！ c}。为了模拟计算，其中只有更新/覆盖的环境的可识别属性被观察到，我们介绍了减少，由一组P。这样的约简隐藏了不能修改由P中的路径表示的扩展表达式的标签。我们写道：实验室• （E，e）−→PCnfOrErr对于（E，e）−→CnfOrErr，其中lab/∈actE（P），CnfOrErr无论是配置还是错误，• （E，e）−→（EJ，eJ）对于r（E，e）−i！→a（EJ，eJ），其中i！a∈actE（P），！P波诺，达米亚尼和吉安尼尼108PPLFLL3CP4CPP1111P111111P· 对于有限个−→P，即−→P，= P，并且！！· 对于有限个−→P，然后是一个−→P-还原步骤，即，−→−→！.例4.3如果我们把例4.2的集合P中的路径作为可观察属性，则图6的计算表示如下：（E，eJJ）=！（EJJ，i;i←y=i. t）=0！（EJJ，i）。4.2互模拟不同环境的可观测属性之间的对应关系被建模为关系RP×PJ，其中P和PJ是有限路径集两个环境E和EJ是R相关的，如果对所有的（p，pJ）∈R，• eexpE（p）=eexpEJ（pJ）=n，对于某个数n，• 或者eexpE（p）= UNDEFINED和eexpEJ（pJ）= UNDEFINED。以下互模拟的概念提升到计算对应R.定义4.4[R-互模拟]设R<$P×PJ，其中P和PJ是有限路集。配置B上的二元关系是R-互模拟，如果（E，e）B（EJ，eJ）意味着：0. E和EJ是R相关的1. （E，e）=！（E，e）表示存在EJ和eJ使得：（EJ，eJ）=！J（EJ，eJ）和d（E，e）B（EJ，eJ）。2. （1）的对称性。3. （E，e）=P（E1，v1）意味着存在E1J（EJ，eJ）=PJ（E1J，vJ1）.4. （3）的对称性。5. （E，e）=Perr意味着：（EJ，eJ）=PJerr。6. （5）的对称性。并且vJ1使得：定义4.4给出了完备格上的单调泛函R.的元素是配置上的关系，按子集包含排序。 这是一个完全格的事实是从以下事实得出的： 配置上任意多个关系的交集仍然是配置上的关系由于FR是单调的，我们可以定义R-双相似性R为最大不动点（由塔斯基定理保证那就是：R=BB 是R-互模拟∼PCPCPP波诺，达米亚尼和吉安尼尼109E EEEE112根（E）例4.5考虑环境J，表达式e，eJ，e0，eJJ，路径集P，PJ，以及在第2节中介绍的关系R(i) 以来（E，e）=！（E，e）=！（E，i），和（EJ，eJ）=！J（EJ，eJ）=0！J（EJ，iJ）哪里P11P2根（E）•1是通过将属性t=4添加到顶级对象并用8覆盖属性x而获得的，• e1=iroot（E）;r oo t. cp←y=r oo t。t，•E1J 通过将属性t=4添加到顶层，对象并使用属性xcoord重写，• eJ1=iroot（E J）;r oo t. 克蓬湾point←xcoord=r oo t. t，• 通过用4覆盖属性y从E1获得E2，并且•E2J 从E1J通过用4覆盖属性ycoord，R互模拟B={（（E，e），（EJ，eJ）），（（E1，e1），（E1J，eJ1）），（（E2，iroot（E）），（E2J，iroot（EJ））}证明了e在E中的行为与eJ在EJ中的行为是等价的（R-双相似）。(ii) 由于（E，e0）=<$P（E，e）和（EJ，e0）=<$PJ（EJ，eJ），B0={（（E，e0），（EJ，e0））}<$B表明e0在E和EJ中具有相同的行为。(iii) 从本例开始时的约简（R）和例4.3的约简（R），我们可以得到R-互模拟B1={（（E，e），（E，eJ J）），（（E1，e1），（E3J J，icp;icp←y=icp. t）），（（E2，Iroot（E）），（E4JJ，Icp））}表明在环境中表达式e具有相同的行为的表达式eJJ。结论和今后的工作在本文中，我们介绍了一种具有可扩展对象的命令式基于对象的演算，该演算对面向Web的脚本语言（如JavaScript）的一些特性进行了建模[9]。我们给出了一个标记的转换语义，其中观察到的动作（由标签表示）是覆盖和添加当前环境中的对象的属性。一个概念的bisimulation，索引的属性，我们要观察，允许证明程序属性有趣的全球计算方案。我们的微积分可以在[3]中编码。然而，一方面，我们只对那些与脚本语言严格相关的功能感兴趣，所以我们更喜欢更小、更集中的演算。另一方面，我们想要一个面向描述历史依赖行为的操作语义，而[3]中的操作语义对于这个目的来说太粗糙PP波诺，达米亚尼和吉安尼尼110我们正在定义一个类型系统，它将捕获在任何环境中使表达式出错的一些错误。该语言的命令式本质，假设所引用的对象是多表的，因为可重写和可扩展，在保持足够的非类型化语言的可扩展性和能够检测一些一般的消息不理解错误之间提出了一个不平凡的权衡。在我们的类型系统中，我们希望捕获类型环境的可变性以及表达式isdef的类型化对环境的依赖性。保持类型系统的可判定性将是主要的关注点。我们还计划将该语言与基于对象的语言的其他功能集成，例如显式委托，这些功能正在DART项目中进行调查[5]。确认我们感谢Sophia Drossopoulou，Christopher Anderson和匿名裁判提供的有用意见和建议。引用[1] M. Abadi和L.卡德利对象的理论。计算机科学中的数学Springer，1996年。[2] V. Bono和M.布列西对象的Lambda演算的匹配Theoretical Computer Science，212（1-2）：101[3] V. Bono和K.费希尔一个带有对象扩展的命令式一阶微积分。在Proc. of ECOOP初步版本已经出现在第五届年度FOOL研讨会的程序中。[4] C. Calcagno，E. Moggi和T.谢尔德安全命令MetaML的封闭类型。函数式编程杂志，出现。[5] DART项目主页。对...感到困惑http://www.disi.unige.it/project/dart/。[6] Visual Basic文档。可在www.example.com上获得http://msdn.microsoft.com/library/。[7] K.费希尔面向对象编程语言的类型系统。斯坦福大学博士论文，1996年。斯坦福计算机科学技术报告编号STAN-CS-TR-98-1602。[8] K.费希尔，F。Honsell和J.C. 米切尔 对象和方法的Lambda演算专业化。Nordic Journal of Computing，1（1）：3-37，1994.一个初步的版本出现在Proc。 LICS'93。[9] D. 弗兰南汉 JavaScript：定义指南。 O’Reilly,[10] R.米尔纳 通信和并发。 普伦蒂斯·霍尔1989年波诺，达米亚尼和吉安尼尼111[11] J. 奥斯特豪特 Tcl和Tk Toolkit。Addison-Wesley，1994年。[12] J. 奥斯特豪特脚本：21世纪的高级编程IEEE计算机杂志，1998年。[13] D.斯坦曼动态双-跨浏览器的动态HTML。可在www.example.com上获得该文档http://www.dansteinman.com/dynduo/。[14] K.A. 怀特 和M.费莱森类型可靠性的句法方法。信息与计算，1994年。A为例在本节中，我们将展示如何在我们的框架中形式化并证明包含JavaScript代码的动态HTML（DHTML）页面是A.1DHTML页面考虑图A.1的DHTML页面，它包含一个块的gif，该块在页面中被定位并可以移动。gif包含在应用了CSS-P（层叠样式表定位）的标记DIV中。这说明了在何处以及如何显示标记的内容。显示属性通过定义标签的STYLE来指定。脚本语言JavaScript [9]用于通过访问和更改显示属性来动画化Web页面。JavaScript代码在显示页面的浏览器函数init在页面加载时执行，函数move绑定到单击页面中按钮的事件单击该按钮时，gif将水平移动5个像素。在代码中，DIV元素被视为一个对象，由其ID中指定的标识符表示。然而，Internet Explorer（IE）和Netscape Navigator（NN）浏览器尽管共享许多兼容对象，但具有不同的域对象模型（DOM）。DOM指定描述文档的预定义对象集，以及如何访问/修改用户定义元素的显示属性。即使在类似的对象，但是，有时会有细微的差异，导致不同的行为取决于所使用的浏览器。这两种浏览器之间的差异之一是，在IE中，每个标签都可以访问，而在NN中，可访问的标签是所有可以定义的标签的子集。属性如何被引用也是不同的。在IE中，属性是通过对象的属性STYLE访问的，而在NN中，它们是直接从对象的标识符访问的。这里我们指的是IE版本5和NN版本4。NN的后续版本，特别是NN版本6，使更多的元素可访问，并且在某种程度上更类似于IE。然而，这两个浏览器之间仍然存在差异。一些技术已经开发出来，使页面是跨浏览器，见[13]。这种技术依赖于检测这种波诺，达米亚尼和吉安尼尼112简体中文⟨SCRIPT⟩publicvoidrun（）{if（document. 层）块=文档。layersif（document. 所有）块=文档。all [”blockDiv“]. 风格;}publicvoid run（）{块myLeft = parseInt（block. left）;block. myLeft =块。myLeft +5;block. 左=块。myLeft;}中文（简体）System. out. println=DIVID=IMGSRC = images/blockImage. GIF动画公司简介公司简介INPUTTYPE=button VALUE=联系我们产品中心中文（简体）图A.1：动态HTML页面我们正在处理的浏览器，以及某些浏览器操作的对象和属性，以及直接引用标记的显示属性的变量的使用。4我们看到这两种技术在函数中的使用-4在[13]一个定义原型对象（类）的库中，可以用来创建跨浏览器页面已定义。使用此库中定义的对象可以屏蔽浏览器之间的差异。波诺，达米亚尼和吉安尼尼113图A.1的初始化。通过测试对象文档是否具有属性all或layers来检测浏览器，并且根据测试的结果，将变量块设置为对与标记相关联的对象的引用，或者对同一对象的属性STYLE的引用。我们还看到，在IE中通过关联数组all（document.all[“blockDiv“];）获得对DIV标记的引用，在NN中通过数组层（document.layers[“blockDiv“];）获得对DIV标记的引用。在函数move中，访问未为对象块定义的属性myLeft会导致将此属性添加到对象。属性left（浏览器已知）被存储为一个数字，后跟字符串px。尽管在这个属性中写入一个数字会自动添加px suprix，但要提取数字部分，我们必须使用函数parseInt。为了避免使用parseInt（block. left）在每个需要数字的表达式中，我们复制属性left，它只是属性myLeft中的一个数字。 我们使用myLeft进行数值计算，并通过将myLeft复制到left中来保持两个属性的同步。最后，注意到脚本行为中有趣的部分是，对象的top、left和width属性（显示属性）是由浏览器监控的，因此更改这些属性会修改页面的外观。在本例中，gif最初定位为左上角距页面左侧150像素，顶部下方150像素单击该按钮可在左侧滑动5像素的gif使用前面提到的技术，这种行为独立于用于显示页面的浏览器A.2正规化为了在我们的框架中形式化图A.1的示例，我们考虑两种环境：IE=[i]→blockDiv = ibD，init = e，move = e，JbD，id→blockall=·· ·， . . . ，<$bD<$→位置=0，左侧=150，顶部=150，和宽度=30英寸]NN=[i] d → [i]document = i]d，blockDiv = i]bD，init = e，move = e]d，i]d→ [i]layers =···，. . 你好，位置=0，左侧=150，顶部=150，宽度=30 mm]其中i=iroot（IE），iJ=iroot（NN），表达式e和eJ定义如下。• e=root←block=e0 with波诺，达米亚尼和吉安尼尼114NNIENN IENNe0=isdef（document，all）？blockDiv. style：isdef（document，layers）blockDiv：blockDiv，• eJ=e1;e2;e3，e 1=根。block← myLeft = root. 块左边，e 2= root。block← myLeft = root. 块myLeft+5，e 3=root。block←left = root. 块我的左边。是IE的DOM中页面标签的定义的翻译。根对象具有属性document（也定义为），它引用具有属性all的对象，该属性是浏览器IE的特征。(For位置属性我们使用0而不是abs，其中abs代表“绝对”。 类似地对于. 注意并表示加载页面之后但执行函数init之前的环境（在IE和NN中表示为顶级对象的方法）。在环境IE中观察到的属性是P={root. blockDiv. 样式的左，根。blockDiv. 样式的上根blockDiv. 样式的宽度}在NN中观察到的是PJ={root. blockDiv. 左，根。blockDiv. 上根blockDiv. width}。我们拥有：ac tIE（P）={i！ blockDi v，IbD！风格！离开！ 到P，IS！宽度h}，以及ac tNN（PJ）={iJ！ blockDi v，IJbD！左，右！ 到p，iJbD！width}。下面的属性表明DHTML页是跨浏览器的。也就是说，在执行init方法之后，再执行任意次数的move方法，在两个环境中都会产生相同的结果。财产对于n≥0，令e（n）= root。init; root。move;. ;根。动“我的天，n对于所有n≥0，我们有（IE，e（n））<$R（NN，e（n）），其中R={（root. blockDiv. 样式的左，根。blockDiv. 左），（根。blockDiv. 样式的上根blockDiv. 顶部），（根。blockDiv. 样式的宽度，根。blockDiv. width）}证据对于n= 0，令IEJ= IE[i：IE（i）[块= is]]和NNJ= NN[iJ：NN（iJ）[块= iJbD]]。为了证明这一结果，证明以下关系就足够了：B0={（（IE，e（0）），（NN，e（0）），（（IEJ，i），（NNJ，iJ））}是互模拟，即B0验证了定义4.4的条件（0）-（6）。很容易看出IE和NN，以及IEJ和NNJ是R相关的，因此条件(0)第4.4节定义 从（IE，e（0））=P（IEJ，i）和（NN，e（0））=P波诺，达米亚尼和吉安尼尼115NNIE NNד我的天，≤ ≤ IENNP`1P`1（J，IJ）我们得出条件（3）和（4）也被验证。最后，条件（1）、（2）、（5）和（6）被平凡地验证。现在考虑n>0的情况。德费恩• IE0=IEJIEn=IEJ[is：IEJ（is）[top=（150 + 5×n），myLeft=（150 + 5×n）]]• NN0=NNJNNn=NNJ[ιbD：NNJ（ιbD）[top=（150 + 5×n），myLeft=（150 + 5×n）]]• e J（n）= root. move;. ;根。移动，n请注意，在n和n的定义中，（150 + 5n）表示相应的整数值（而不是表达式）。为了证明这个结果，我们必须证明，对于所有n>0，Bn={（（IE，e（n）），（NN，e（n）），（（IEn，i），（NNn，iJ））}1≤i≤n−1{（（IEi，eJ（n−i）），（NNi，eJ（n−i）}是互模拟 很容易看出，对于所有i，1in， i和i是R相关，因此定义4.4的条件（0）成立。此外，我们有：• （IE，e（n））=！（IE，eJ（n−1））=0！n−1P··x·（IEn，i），以及• （NN，e（n））=0！（NN，eJ（n−1））=0！n−1P··x·（NNn，J）。因此，定义4.4的条件（1）和（2）也得到了验证。最后，条件（3）-（6）被简单地验证。证明到此结束✷
我的内容管理
展开
