An overview of the K semantic framework
An overview of the K semantic framework
复制标题
DOI：
10.1016/j.jlap.2010.03.012
复制
发表时间：
2010-08-01
影响因子：
--
通讯作者：
Serbanuta, Traian Florin
中科院分区：
文献类型：
--
作者：
Rosu, Grigore;Serbanuta, Traian Florin
K 是一个可执行的语义框架，其中可以使用配置、计算和规则来定义编程语言、演算以及类型系统或形式分析工具。配置以称为单元的单元组织系统/程序状态，这些单元被标记并且可以嵌套。计算具有“计算意义”，作为对计算任务（例如程序片段）进行排序的特殊嵌套列表结构；特别是，计算扩展了原始语言或微积分语法。 K（重写）规则通过明确他们读、写或不关心术语的哪些部分来概括传统的重写规则。这种区别使得 K 成为定义真正并发语言或演算的合适框架，即使存在共享。由于计算可以像重写环境中的任何其他术语一样处理，也就是说，它们可以匹配、从原始术语中的一个位置移动到另一个位置、修改甚至删除。 K 特别适合定义控制密集型语言功能，例如突然终止、异常或 call/cc。本文概述了 K 框架：它是什么、如何使用以及到目前为止已在何处使用。它还提出并讨论了CHALLENGE的K定义，CHALLENGE是一种旨在挑战和暴露现有语义框架局限性的编程语言。 (C) 2010 Elsevier Inc. 保留所有权利。
K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of configurations, computations and rules. Configurations organize the system/program state in units called cells, which are labeled and can be nested. Computations carry "computational meaning" as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax. K (rewrite) rules generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about. This distinction makes K a suitable framework for defining truly concurrent languages or calculi, even in the presence of sharing. Since 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, modified, or even deleted. K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions, or call/cc.This paper gives an overview of the K framework: what it is, how it can be used, and where it has been used so far. It also proposes and discusses the K definition of CHALLENGE, a programming language that aims to challenge and expose the limitations of existing semantic frameworks. (C) 2010 Elsevier Inc. All rights reserved.