《一个框架时序逻辑程序设计语言》由会员分享，可在线阅读，更多相关《一个框架时序逻辑程序设计语言（22页珍藏版）》请在金锄头文库上搜索。
1、A Framed Temporal Logic Programming LanguageZhenhua DuanMaciej Koutny Computer SchoolDepartment of Computing Science Xidian UniversityUniversity of Newcastle upon Tyne Xi0an 710071 P.R.ChinaNewcastle upon Tyne NE1 7RU, U.K. Maciej.Koutnynewcastle.ac.ukAbstractWe discuss the projection temporal logic
2、 (PTL), based on a primitive projection operator, prj . Aframing technique is also presented, using which a synchronization operator, await, is defined within the underlying logic. A framed temporal logic programming language (FTLL) is presented. To illustrate how to use both the language and framin
3、g technique, some examples are given. Keywords: Temporal logic, Temporal logic programming, Frame, Projection, Concurrency1IntroductionTemporal logic has been introduced in order to the verify behavioural properties of programs. This hasintroduced an additional complication since one had to deal wit
4、h three different notations: one for a pro- gramming language, one for a logic framework, and yet another for the description of program properties. It has therefore been suggested that a subset of temporal logic be used as the foundational basis for a pro-gramming language 15. This means that writi
5、ng of programs, specification of the properties of programs,and the verification of program properties, could all be treated within the same notation. However, thereare some aspects of programming in temporal logic notation that have not yet received sufficient attention, notably the problem of sync
6、hronization and communication. Typically, temporal logic programming languages, e.g., XYZ/E 5, 6, Tempura 4, TLA 3 and METATEM 1, employ logic conjunction () as a basic parallel operator for concurrent computations. An advantageof the conjunction construct is its simplicity. It seems appropriate for
7、 dealing with fine-grained parallel operations that proceed in lock-step. However, processes combined through the conjunction operator share all the states and therefore may interfere with one another.7 introduced a new projection operator, (p1,.,pm)prj q, which can be thought of as a combination of
8、 the standard parallel and projection operators. Intuitively, it means that q is executed in parallel with p1;.;pmover an interval obtained by taking the endpoints (rendezvous points) of the intervals over which p1,.,pmare executed. The projection construct permits the processes p1,.,pm,q to be auto
9、nomous, with each process having the right to specify theSupport by the National Natural Science Foundation of China under Grant No.60373103, the SRFDP Grant 20030701015and the Grant SYSKF0407 from Lab. Computer Science, ISCAS.1_2interval over which it is executed. In particular, the sequence of pro
10、cesses, p1,.,pmand process q mayterminate at different time points. Although the communication between processes is still based on shared variables, the communication and synchronization only take place at the rendezvous points (global states),otherwise they are executed independently. The new proje
11、ction operator also enables the specification ofprogram execution using different time scales. Another problem that must be dealt with in temporal logic programming is that of communication between concurrent processes. Some models of concurrency involve shared (programming) variables, some involve
12、synchronous message passing (e.g. CCS 8 and CSP 9), and some involve asynchronous channels.In temporal logic programming languages, such as XYZ/E 5, 6, Tempura 4, METAMET 1 and TOKIO 2, the communication between parallel components is based on shared variables. Similarly as many concurrent programmi
13、ng languages 10, to synchronize communication between parallel processes in a concurrent program with the shared variable model (e.g., when solving the mutual exclusion problem), a synchronization construct, await(c) or some equivalent is required. The meaning of await(c) is simple: it changes no va
14、riables, but waits until the condition c becomes true, at which point it terminates. In a sequential program, an await statement is useless, since if c is currently false it will remain so forever. However, within a concurrent program this statement makes perfect sense since another process, acting
15、in parallel, may cause c to become true.Defining await(c) is difficult without some kind of a framing construct. However, there is a problem which is caused by the fact that in temporal logic the values of variables are not inherited automatically from onestate to another. Yet, to implement await(c)
16、, one requires some kind of indefinite stability, since one cannot know at the point of use how long the waiting will last. At the same time one must also allow variables to change, so that an external process can modify the Boolean parameter and it can eventually become true. Framing is concerned with how the value of
