检索结果-内蒙古大学图书馆

12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

作者： Aceto, Luca Gorla, Daniele Lybech, Stian Hamdaqa, Mohammad Reykjavik Univ Dept Comp Sci Reykjavik Iceland Gran Sasso Sci Inst Laquila Italy Sapienza Univ Roma Rome Italy Polytech Montreal Montreal PQ Canada

ISBN: (纸本)9783031737084;9783031737091

We continue the development of TINYSOL, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TINYSOL with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TINYSOL, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker.

关键词： Smart-contract language Type system Static analysis semantics of programming languages

来源：评论

学校读者我要写书评

暂无评论

A DENOTATIONAL APPROACH FOR TYPE-CHECKING IN OBJECT-ORIENTED programming-languages

引用

COMPUTER languages 1993年第1期19卷 19-40页

作者： IERUSALIMSCHY, R Departamento de Inform&aacute tica Pontificia Universidade Cat&oacute lica 22453-900 Rio de Janeiro Brazil

Starting with a pragmatical (but formal) definition of type in object-oriented languages, this paper proposes a method to test type safety in this kind of language. We say that a language is (type) safe if it ensures that, during the execution of a correct program, every message sent to an object is matched by an appropriate method. We define a ''typical'' object oriented programming language, featuring multiple inheritance, recursive types, and separation between specifications and implementations. Then, we give a formal definition for its type system, and a denotational semantics for the execution of the language, based on message passing. Finally, we formally prove that our language is type safe. Along the progress of the work, better understanding is gained about many problems related with type systems in object-oriented languages.

关键词： semantics of programming languages TYPE SYSTEMS OBJECT ORIENTED programming

来源：评论

学校读者我要写书评

暂无评论

A VIEW OF programming-languages AS SYMBIOSIS OF MEANING AND COMPUTATIONS

引用

NEW GENERATION COMPUTING 1985年第1期3卷 71-100页

作者： VODA, PJ UNIV BRITISH COLUMBIA DEPT COMP SCIVANCOUVER V6T 1W5BCCANADA

Function and logic programming languages are understood as terms, resp. formulas, of a first order theory. This theory gives meaning to programs and allows reasoning about programs within full predicate logic possibly using quantifiers and induction. The operational semantics of programming languages is given by deductively restricted subtheories of the meaning theory in such a way that the computation sequences are in a one-to-one correspondence with proofs in subtheories. Moreover, meaning is invariant to computations as everything provable in a subtheory is required to be a theorem of the meaning theory. The questions of deadlocks and termination of programs are thus reduced to the proof-theoretical questions of existence of proofs in the subtheories.

关键词： semantics of programming languages Operational semantics Functional languages Logic programming Formal Theories

来源：评论

学校读者我要写书评

暂无评论

Toward Analysis and Bug Finding in JavaScript Web Applications in the Wild

引用

IEEE SOFTWARE 2019年第3期36卷 74-82页

作者： Ryu, Sukyoung Park, Jihyeok Park, Joonyoung Korea Adv Inst Sci & Technol Sch Comp Daejeon South Korea

We present our journey to analyze and find bugs in JavaScript web applications in the wild. We describe technical challenges in analyzing them and our solutions to address the challenges via a series of open source an... 详细信息

关键词： Internet Java Program Debugging Public Domain Software Bug Finding Java Script Web Applications Technical Challenges Open Source Analysis Frameworks Scalable Analysis Framework ECMA Script Family SAFE Computer Bugs Browsers Object Recognition Java Electronic Publishing Computer Applications Program Analysis semantics of programming languages Logics And Meanings Of Programs Theory Of Computat Software Software Engineering Testing And Debugging

来源：评论

学校读者我要写书评

暂无评论

The origins of structural operational semantics

引用

JOURNAL OF LOGIC AND ALGEBRAIC programming 2004年第SUPPL.期60-1卷 3-15页

作者： Plotkin, GD Univ Edinburgh Sch Informat Lab Fdn Comp Sci Edinburgh EH9 3JZ Midlothian Scotland

We review the origins of structural operational semantics. The main publication 'A Structural Approach to Operational semantics,' also known as the 'Aarhus Notes,' appeared in 1981 [G.D. Plotkin, A structural approach to operational semantics, DAIMI FN-19, Computer Science Department, Aarhus University, 1981]. The development of the ideas dates back to the early 1970s, involving many people and building on previous work on programming languages and logic. The former included abstract syntax, the SECD machine, and the abstract interpreting machines of the Vienna school;the latter included the lambda-calculus and formal systems. The initial development of structural operational semantics was for simple functional languages, more or less variations of the lambda-calculus;after that the ideas were gradually extended to include languages with parallel features, such as Milner's CCS. This experience set the ground for a more systematic exposition, the subject of an invited course of lectures at Aarhus University;some of these appeared in print as the 1981 Notes. We discuss the content of these lectures and some related considerations such as 'small state' versus 'grand state,' structural versus compositional semantics, the influence of the Scott-Strachey approach to denotational semantics, the treatment of recursion and jumps, and static semantics. We next discuss relations with other work and some immediate further development. We conclude with an account of an old, previously unpublished, idea: an alternative, perhaps more readable, graphical presentation of systems of rules for operational semantics. (C) 2004 Elsevier Inc. All rights reserved.

关键词： semantics of programming languages (structural) operational semantics structural induction (labelled) transition systems lambda-calculus concurrency big step semantics small-step semantics abstract machines static semantics

来源：评论

学校读者我要写书评

暂无评论

semantics-based generation of verification conditions via program specialization

引用

SCIENCE OF COMPUTER programming 2017年 147卷 78-108页

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. Univ G dAnnunzio DEC Viale Pindaro 42 I-65127 Pescara Italy Univ Roma Tor Vergata DICII Via Politecn 1 I-00133 Rome Italy CNR IASI Via Taurini 19 I-00185 Rome Italy

We present a method for automatically generating verification conditions for a class of imperative programs and safety properties. Our method is parametric with respect to the semantics of the imperative programming language, as it generates the verification conditions by specializing, using unfold/fold transformation rules, a Horn clause interpreter that encodes that semantics. We define a multi-step operational semantics for a fragment of the C language and compare the verification conditions obtained by using this semantics with those obtained by using a more traditional small-step semantics. The flexibility of the approach is further demonstrated by showing that it is possible to easily take into account alternative operational semantics definitions for modeling additional language features. We have proved that the verification condition generation takes a number of transformation steps that is linear with respect to the size of the imperative program to be verified. Also the size of the verification conditions is linear with respect to the size of the imperative program. Besides the theoretical computational complexity analysis, we also provide an experimental evaluation of the method by generating verification conditions using the multi-step and the small-step semantics for a few hundreds of programs taken from various publicly available benchmarks, and by checking the satisfiability of these verification conditions by using state-of-the-art Horn clause solvers. These experiments show that automated verification of programs from a formal definition of the operational semantics is indeed feasible in practice. (C) 2016 Elsevier B.V. All rights reserved.

关键词： Horn clauses Program verification Program specialization semantics of programming languages Software model checking

来源：评论

学校读者我要写书评

暂无评论

MECHANIZING SOME ADVANCED REFINEMENT CONCEPTS

引用

FORMAL METHODS IN SYSTEM DESIGN 1993年第1-2期3卷 49-81页

作者： VONWRIGHT, J HEKANAHO, J LUOSTARINEN, P LANGBACKA, T UNIV CAMBRIDGE COMP LABCAMBRIDGE CB2 3QGENGLAND

We describe how the HOL theorem prover can be used to check and apply rules of program refinement. The rules are formulated in the refinement calculus, which is a theory of correctness preserving program transformations. We embed a general command notation with a predicate transformer semantics in the logic of the HOL system. Using this embedding, we express and prove rules for data refinement and superposition refinement of initialized loops. Applications of these proof rules to actual program refinements are checked using the HOL system, with the HOL system generating these conditions. We also indicate how the HOL system is used to prove the verification conditions. Thus, the HOL system can provide a complete mechanized environment for proving program refinements.

关键词： PROGRAM VERIFICATION semantics of programming languages DEDUCTION AND THEOREM PROVING

来源：评论

学校读者我要写书评

暂无评论

Software meta-language engineering and CBS

引用

JOURNAL OF COMPUTER languages 2019年 50卷 39-48页

作者： Mosses, Peter D. Swansea Univ Dept Comp Sci Computat Foundry Bay Campus Swansea SA1 8EN W Glam Wales Delft Univ Technol Programming Languages EEMCS POB 5031 NL-2600 GA Delft Netherlands

The SLE conference series is devoted to the engineering principles of software languages: their design, their implementation, and their evolution. This paper is about the role of language specification in SLE. A precise specification of a software language needs to be written in a formal meta-language, and it needs to co-evolve with the specified language. Moreover, different software languages often have features in common, which should provide opportunities for reuse of parts of language specifications. Support for co-evolution and reuse in a meta-language requires careful engineering of its design. The author has been involved in the development of several meta-languages for semantic specification, including action semantics and modular variants of structural operational semantics (MSOS, I-MSOS). This led to the PLanCompS project, and to the design of its meta-language, CBS, for component-based semantics. CBS comes together with an extensible library of reusable components called 'funcons', corresponding to fundamental programming constructs. The main aim of CBS is to optimise co-evolution and reuse of specifications during language development, and to make specification of language semantics almost as straightforward as context-free syntax specification. The paper discusses the engineering of a selection of previous meta-languages, assessing how well they support co-evolution and reuse. It then gives an introduction to CBS, and illustrates significant features. It also considers whether other current meta-languages might also be used to define an extensible library of funcons for use in component-based semantics.

关键词： semantics of programming languages Meta-languages Modularity

来源：评论

学校读者我要写书评

暂无评论

KLAIM: A kernel language for agents interaction and mobility

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1998年第5期24卷 315-330页

作者： De Nicola, R Ferrari, GL Pugliese, R Univ Florence Dipartimento Sistemi & Informat I-50134 Florence Italy Univ Pisa Dipartimento Informat I-56100 Pisa Italy

We investigate the issue of designing a kernel programming language for mobile computing and describe KLAIM, a language that supports a programming paradigm where processes, like data, can be moved from one computing environment to another. The language consists of a core Linda with multiple tuple spaces and of a set of operators for building processes. KLAIM naturally supports programming with explicit localities. Localities are first-class data (they can be manipulated like any other data), but the language provides coordination mechanisms to control the interaction protocols among located processes. The formal operational semantics is useful for discussing the design of the language and provides guidelines for implementations. KLAIM is equipped with a type system that statically checks access rights violations of mobile agents. Types are used to describe the intentions (read, write, execute, etc.) of processes in relation to the various localities. The type system is used to determine the operations that processes want to perform at each locality, and to check whether they comply with the declared intentions and whether they have the necessary rights to perform the intended operations at the specific localities. Via a series of examples, we show that many mobile code programming paradigms can be naturally implemented in our kernel language. We also present a prototype implementaton of KLAIM in Java.

关键词： programming languages mobile code languages semantics of programming languages language design coordination models

来源：评论

学校读者我要写书评

暂无评论

SEMANTIC EQUIVALENCE OF COVERING ATTRIBUTE GRAMMARS

引用

INTERNATIONAL JOURNAL OF COMPUTER & INFORMATION SCIENCES 1979年第6期8卷 523-539页

作者： BOCHMANN, GV Département d'Informatique et de Recherche Operationnelle Université de Montréal Montréal Canada

This paper investigates some methods for proving the equivalence of different language specifications that are given in terms of attribute grammars. Different specifications of the same language may be used for different purposes, such as language definition, program verification, or language implementation. The concept of syntactic coverings is extended to the semantic part of attribute grammars. Given two attribute grammars, the paper discusses several propositions that give sufficient conditions for one attribute grammar to be semantically covered by the other one. These tools are used for a comparison of two attribute grammars that specify syntax and semantics of mixed-type expressions. This example shows a trade-off between the complexity of syntactic and semantic specifications. Another example discussed is the equivalence of different attribute grammars for the translation of the while-statement, as used in compilers for top-down and bottom-up syntax analysis.

关键词： attribute grammars compiler correctness coverings equivalent semantic specifications formal specification of semantics Semantic equivalence semantics of programming languages

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：