FunKons: Component-Based Semantics in K

1999

By paying more attention to semantics-based tool generation, programming language semantics can significantly increase its impact. Ultimately, this may lead to "Language Design Assistants" incorporating substantial amounts of semantic knowledge.

Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '80, 1980

about a year I have worked on a semantic specification for the C programming language My objecti~e was to construct a readable and precise specification of C. aimed at compiler writers, maintamers, and language pundm, This paper is a report on the project, * UNIX is a trademark of Bell Laboratories.

2007

Providing proper modularity is one of the major challenges in software development. In the context of programming language implementation, two key factors impede the modularization process in a compiler system: First, the parser, as the core of the language implementation, usually is specified in a non-decomposable style such that it must

2000

Programming language semantics has lost touch with large groups of potential users [39]. Among the reasons for this unfortunate state of affairs, one stands out. Semantic results are rarely incorporated in practical systems that would help language designers to implement and test a language under development, or assist programmers in answering their questions about the meaning of some language feature not properly documented in the language's reference manual.

Journal of Computer Science and Technologie, 2002

There are two main activities in Component-Based Development: component development, where we build libraries for general use, and component integration, where we assemble an application from existing components. In this work, we analyze how to apply algebraic specifications with refinement to component development. So we restrict our research to the use of modules that are described as class expressions in a formal specification language, and we present several refinement steps for component ...

HAL (Le Centre pour la Communication Scientifique Directe), 2017

This report documents how we have implemented a trace generator for the Circus specification language using K, a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. This implementation is based on the operational semantics of Circus, that we have revisited to make it exploitable with K. The motivation of this work is the development of a test generation environment for Circus. Moreover, it may provide some inspiration to the developers of tools for specification languages based on process algebras.

2000

Abstract: We specify the dynamic semantics of an object oriented programminglanguage in an incremental way. We begin with a simple language of arithmeticand boolean expressions. Then, we add functional abstractions, localdeclarations, references and assignments obtaining a functional language withimperative features. We finally add objects, classes and subclasses to obtain aprototypical object oriented language with dynamic binding.

International Refinement Workshop & Formal Methods Pacific’98, 1998

Abstract. This paper presents an approach to formalize COM. Despite its importance, COM still does not have a formal specification. In order to understand the COM's informal rules better, the COMEL language is being introduced. We formalized some of the important COM's rules and present COMEL's abstract syntax, formal semantics and subject reduction theorem.

Lecture Notes in Computer Science, 2004

Component based design and development of software is one of the most challenging issues in software engineering. In this paper, we adopt a somewhat simplified view of software components and discuss how they can be conveniently modelled in a framework that provides a modular approach to formal software development by means of stepwise refinement. In particular we take into account an observational interpretation of requirements specifications and study its impact on the definition of the semantics of specifications of (parametrized) components. Our study is carried out in the context of Casl architectural specifications.

We define a framework of components based on Java-like languages, where components are binary mixin modules. Basic components can be obtained from a collection of classes by compiling such classes in isolation; for allowing that, requirements in the form of type constraints are associated with each class to specify the contexts where classes can be safely used. Requirements are specified by the user who, however, is assisted by the compiler which can generate missing constraints essential to guarantee type safety. Basic components can be composed together thanks to a set of expressive typed operators; thanks to soundness results, such composition is always type safe. The framework is designed as a separate layer which can instantiated on top of any Javalike language. The flexibility offered by constraints and the expressive power of the operators make the framework particularly suitable for reusing and extending software components in a modular way.