K语义框架：一种可执行的编程语言定义工具

36 浏览量更新于2024-07-14 收藏 676KB PDF 举报

"The K Semantic Framework (CS422-Spring-2010-K)-计算机科学" 《K语义框架》是计算机科学领域的一份重要文献，主要介绍了K，一个基于重写技术的可执行语义框架。这个框架首次由作者在2003年秋季伊利诺伊大学厄巴纳-香槟分校（UIUC）的编程语言设计课程中提出，目的是利用Maude在重写逻辑中定义并发语言。自那时起，K已被广泛应用于教学、研讨会以及研究工作中。 K的核心思想是通过配置、计算和规则来定义编程语言、计算理论以及类型系统或形式分析工具。配置是组织系统/程序状态的基本单元，称为细胞，它们带有标签并且可以嵌套。这些细胞共同构成了程序的结构和状态。计算是K中的特殊结构，承载着“计算意义”。具体来说，计算是嵌套列表术语，它们序列化了计算任务，比如程序的片段。特别是，计算扩展了原始编程语言或计算体系的语法。 K规则（重写规则）是对传统重写规则的泛化，它明确指出规则作用于配置的哪些部分。这种设计使得K能够精确地描述和执行语言的语义，同时允许对语言的各个方面进行修改和扩展。例如，通过定义新的规则，K可以支持新的运算符、控制结构或异常处理机制。 K框架的一个显著优点是它的可执行性。定义在K中的语言或计算模型可以直接运行，从而可以进行形式验证、模拟和分析。此外，由于K的灵活性和模块化，它能够处理各种复杂性，包括并发性、异步通信和动态行为。自2003年以来，K在教学中的应用已经证明了其作为教育工具的有效性，帮助学生深入理解编程语言的内部工作原理。在研讨会中，K被用来探讨新的语言设计概念和实现技术。而在研究领域，K作为一种强大的形式化方法，被用于开发和验证新的编程语言特性，推动了编译器、解释器和验证工具的进步。总而言之，《K语义框架》提供了构建和理解编程语言的创新方法，通过其可执行的语义，促进了编程语言理论与实践的紧密联系，为计算机科学教育和研究提供了有力的工具。

concepts of category theory, logics, or type theory, in order to use it. Also, it should have good

data representation capabilities and should allow proofs of theorems about programming languages

that are easy to comprehend. Additionally, a framework providing support for parsing programs

directly in the desired language syntax may be desirable to one requiring the implementation of an

additional, external to the deﬁnitional setting, parser.

The nine requirements above are nevertheless ambitious. Some proponents of existing language

deﬁnitional frameworks may argue that their favorite framework has these properties; however,

a careful analysis of existing language deﬁnitional frameworks reveals that they actually fail to

satisfy some of these ideal features (we discussed several such frameworks and their limitations in

Chapter 3). Others may argue that their favorite framework has some of the properties above, the

“important ones”, declaring the other properties either “not interesting” or “something else”. For

example, one may say that what is important in one’s framework is to get a dynamic semantics of a

language, but its (model-theoretical) algebraic denotational semantics, proving properties about

programs, model checking, etc., are “something else” and therefore are allowed to need a diﬀerent

“encoding” of the language. Our position is that an ideal language deﬁnitional framework should not

compromise any of the nine requirements above.

Whether K satisﬁes all the requirements above or not is, and probably will always be, open.

What we can mention with regards to this aspect, though, is that K was motivated and stimulated

by the observation that the existing language deﬁnitional frameworks fail to fully satisfy these

minimal requirements; consequently, K’s design and development were conducted aiming explicitly

to fulﬁll all nine requirements discussed above, promoting none of them at the expense of others.

5.2 K Overview by Example

Here we brieﬂy describe the K framework, what it oﬀers and how it can be used. We use as concrete

examples the IMP language (Section 3.1) and its extension IMP++ (Section 3.8), discussed in

Chapter 3 in the context of the various existing language deﬁnitional frameworks. We deﬁne both

an executable semantics and a type system for these languages. The type system is included mainly

for demonstration purposes, to show that one can use the same deﬁnitional framework, K, to deﬁne

both formal language semantics and language abstractions. The role of this section is threefold:

ﬁrst, it gives the reader a better understanding of the K framework before we proceed to deﬁne it

rigorously in the remainder of this chapter; second, it shows how K avoids the limitations of the

various more conventional semantic approaches discussed in Chapter 3; and third, it shows that

K is actually easy to use, in spite of the intricate K concurrent abstract machine technicalities

discussed in Section 5.4 — indeed, users of the K framework need not be familiar with all those

intricate details, the same way users of a concurrent programming language need not be aware

of the underlying details of the concurrent computing architecture on which their programs are

executed. In fact, in this section we make no distinction between the K rewrite abstract machine

and the K technique, refering to these collectively as “the K framework”, or more simply just “K”.

Programming languages, calculi, as well as type systems or formal analyzers can be deﬁned in K

by making use of special, potentially nested (K) cell structures, and (K) (rewrite) rules. There are

two types of K rules: computational rules, which count as computational steps, and structural rules,

which do not count as computational steps. The role of the structural rules is to rearrange the term

so that the computational rules can apply. K rules are unconditional (they can be thought of as

rule schemata and may have ordinary side conditions, though), and they are context-insensitive, so

280

K rules apply concurrently as soon as they match, without any contextual delay or restrictions.

One sort has a special meaning in K, namely the sort

of computations. The intuition for terms

of sort

is that they have computational contents, such as programs or fragments of programs have;

indeed, computations extend the syntax of the original language. Computations have a list structure

with “

↷

” (read “followed by”) concatenating two computations and “

⋅

” the empty computation; the

list structure captures the intuition of computation sequentialization. Computations give an elegant

and uniform means to deﬁne and handle evaluation contexts (Section 3.8.1) and/or continuations

[

]. Indeed, a computation “

v ↷c

” can be thought of as “

c[v]

, that is, evaluation context

applied

” or as “passing

to continuation

”. Computations can be handled like any other terms in

a rewriting environment, that is, they can be matched, moved from one place to another in the

original term, modiﬁed, or even deleted. A term may contain an arbitrary number of computations,

which can evolve concurrently; they can be thought of as execution threads. Rules corresponding to

inherently sequential operations (such as lookup/assignment of variables in the same thread) must

be designed with care, to ensure that they are applied only at the top of computations.

The distinctive feature of K compared to other term rewriting approaches in general and to

rewriting logic (Section 2.7) in particular, is that K allows rewrite rules to apply concurrently even

in cases when they overlap, provided that they do not change the overlapped portion of the term.

This allows for truly concurrent semantics to programming languages and calculi. For example,

two threads that read the same location of memory can do that concurrently, even though the

corresponding rules overlap on the store location being read. The distinctive feature of K compared

to other frameworks for true concurrency, like chemical abstract machines (Section 3.6) or membrane

systems (Section 9.7), is that rewrite rules can match across and inside multiple cells and thus

perform changes many places at the same time, in one concurrent step.

K achieves, in one uniform framework, the beneﬁts of both the chemical abstract machines

(CHAMs; Section 3.6) and reduction semantics with evaluation contexts (RSEC; Section 3.8.1),

at the same time avoiding what might be called the “rigidity to chemistry” of the former and the

“rigidity to syntax” of the latter. Any CHAM and any RSEC deﬁnition can be captured in K with

minimal (in our view zero) representational distance. K can support concurrent language deﬁnitions

with either an interleaving or a true concurrency semantics.

Like the other semantic approaches that can be represented in rewriting logic (Chapter 3),

K can also be represented in rewriting logic and thus K deﬁnitions can be executed on existing

rewrite engines, thus providing “interpreters for free” directly from formal language deﬁnitions;

additionally, general-purpose formal analysis techniques and tools developed for rewriting logic, such

as state space exploration for safety violations or model-checking, give us corresponding techniques

and tools for the deﬁned languages, at no additional development cost. Unlike the other semantic

approaches whose representations in rewriting logic are faithful, in that the resulting rewriting logic

theories are step-for-step equivalent with the original deﬁnitions, K cannot be captured faithfully

by rewriting logic in any natural way. On the one hand, there is no clear way to represent the K

structural rules in rewriting logic in a general way that properly captures the intuition that the K

computational rules take place “modulo” the structural ones; this results in the rewrite logic theory

to potentially miss some of the non-deterministic behaviors of the original K deﬁnition. On the

other hand, the corresponding rewrite logic theory may need more interleaved steps in order to

capture one concurrent step in the original K deﬁnition; this results in the rewrite logic theory to

potentially miss some of the concurrent behaviors of the original K deﬁnition.

281

剩余42页未读，继续阅读

weixin_38607908

粉丝: 7
资源: 935

K语义框架：一种可执行的编程语言定义工具

Semantic-UI-master.zip

前端开源库-semantic-release-plugin-decorators

The Model-Driven Semantic Web-SSI-EW-2005-08-16

Open-Semantic-Framework-Installer:用于安装，更新和配置Open Semantic Framework实例的命令行工具

Semantic Time Framework-开源

responsive-semantic-html5-template

Semantic-UI-CSS-master.zip_Semantic-UI-master_semantic css_steep

4-SemanticWeb_RDF-Reasoning

Semantic Graph Mediawiki Extension-开源

IBM Semantic Layered Research Platform-开源

最新资源