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

A Theorem Proving Approach to programming language semantics 23

A Theorem Proving Approach to Programming Language Semantics

IEEE/ACM 45th International Conference on Software Engineering - Software Engineering Education and Training (ICSE-SEET)

作者： Roy, Subhajit Indian Inst Technol Kanpur Kanpur India

ISBN: (纸本)9798350322590

The semantics of programming languages is one of the core topics in computer science. This topic is formalism-heavy and requires the student to attempt numerous proofs for a deep understanding. We argue that modern theorem provers are excellent aids to teaching and understanding programming language semantics. As pen-and-paper proofs get automated via the theorem prover, it allows an experiment-driven strategy at exploring this topic. This article provides an encoding of the semantics of the WHILE language in the most popular styles-operational, denotational, and axiomatic-within the F* proof assistant. We show that once the program and its semantics are encoded, modern proof assistants can prove exciting language features with minimal human assistance. We believe that teaching programming languages via proof assistants will not only provide a more concrete understanding of this topic but also prepare future programming language researchers to use theorem provers as fundamental tools in their research and not as an afterthought.

关键词： Computer Science Education Interactive Proof Assistants programming language semantics Theorem Proving

来源：评论

学校读者我要写书评

暂无评论

Label-Based programming language semantics in K Framework with SDF 14th

Label-Based Programming Language Semantics in K Framework wi...

引用

14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

作者： Bogdanas, Denis Alexandru Ioan Cuza Univ Fac Comp Sci Iasi Romania

ISBN: (纸本)9780769549347;9781467350266

A programming language definition consists of two parts: syntax and semantics. K Framework is an actively developed formalism aimed to address the semantics part. While K has its own capabilities to define syntax and to perform parsing, those are often not expressive enough to handle real world programming languages. Therefore K Framework was designed to be connected to an external parser. In this case the semantics is defined over the representation of programs as AST (Abstract Syntax Tree), and is called label-based. This technique was successfully used to define C language. In this paper we present a parser generator which accepts as input a grammar in SDF format, and produces a parser ready to be integrated with K. We illustrate the methodology of defining a language using the generated parser based on an example. The example definition emphasizes distinctive features of the integration of SDF syntax and K semantics. It also illustrates syntax constructs which are difficult to handle with K Framework alone, but are straightforward to express in SDF + K combination.

关键词： C language context-free grammars programming language semantics

来源：评论

学校读者我要写书评

暂无评论

Syntax and operational semantics of a probabilistic programming language with scopes

引用

JOURNAL OF MATHEMATICAL PSYCHOLOGY 2016年 74卷 46-57页

作者： Bruza, Peter D. QUT Sch Informat Syst GPO Box 2434 Brisbane Qld Australia

Dzhafarov and Kujala (2015) have introduced a contextual probability theory called Contextuality-by-Default (C-b-D) which is based on three principles. The first of these principles states that each random variable should be automatically labelled by all conditions under which it is recorded. The aim of this article is to relate this principle to block structured computer programming languages where variables are declared local to a construct called a "scope". Scopes are syntactic constructs which correspond to the notion of condition used by C-b-D. In this way a variable declared in two scopes can be safely overloaded meaning that they can have the same label but preserve two distinct identities without the need to label each variable in each condition as advocated by C-b-D. By means of examples, the notion of a probabilistic-program, or P-program, is introduced which is based on scopes. The semantics of P-programs will be illustrated using the well known relational database language SQL which provides an efficient and understandable operational semantics. A core issue addressed is how to construct a single probabilistic model from the various interim probability distributions returned by each syntactic scope. For this purpose, a probabilistic variant of the natural join operator of relational algebra is used to "glue" together interim distributions into a single distribution. More generally, this article attempts to connect contextuality with probabilistic programming by means of relational database theory. (C) 2016 Published by Elsevier Inc.

关键词： Probabilistic programming Probabilistic modelling programming language semantics Contextuality Contextuality-by-Default

来源：评论

学校读者我要写书评

暂无评论

Model-driven approach to developing domain functional requirements in software product lines

引用

IET SOFTWARE 2012年第4期6卷 391-401页

作者： Guo, J. Wang, Y. Zhang, Z. Nummenmaa, J. Niu, N. Shanghai Jiao Tong Univ Dept Comp Sci & Engn Shanghai 200240 Peoples R China Univ Tampere Sch Informat Sci FIN-33014 Tampere Finland Mississippi State Univ Dept Comp Sci & Engn Mississippi State MS 39762 USA

Existing product requirements form a rich source for domain requirements analysis in software product lines (SPLs). Most existing domain analysis techniques depend on domain experts' experience and manual operation to identify the commonalities and variabilities of product requirements. They often demand a high level of manual effort and a large up-front investment, which can present a prohibitive barrier for SPL adoption. This study proposes a model-driven approach to semi-automatically derive domain functional requirements (DFRs) from product functional requirements (PFRs). Based on the linguistic characterisation of a domain's action-oriented concerns, the authors apply Fillmore's semantic framework to functional requirements and define metamodels for PFRs and DFRs. Functional requirements of existing products are constructed as corresponding PFR models. Following the proposed merging and refinement rules, the authors approach automates the transformation from PFR models into DFR models by merging the same or similar PFRs and analysing their commonality and variability. The resulting DFR models can serve as an initial basis of the SPL. The authors demonstrate the authors approach using an example of a home security system (HSS) SPL and give a preliminary evaluation. The authors approach provides a rigorous model-based support for DFRs development and complements existing domain analysis techniques with less time and effort.

关键词： Software management linguistic characterisation domain functional requirement analysis Formal languages and computational linguistics Software engineering techniques software development management formal verification software product lines domain expert experience PFR metamodel domain action oriented concerns DFR metamodel SPL adoption Formal methods home security system model-driven approach Fillmore's semantic framework up-front investment programming language semantics product functional requirements

来源：评论

学校读者我要写书评

暂无评论

Full abstraction for PCF

引用

INFORMATION AND COMPUTATION 2000年第2期163卷 409-470页

作者： Abramsky, S Jagadeesan, R Malacaria, P Univ Oxford Oxford England Loyola Univ Chicago IL 60611 USA Queen Mary Univ London London E1 4NS England

An intensional model for the programming language PCF is described in which the types of PCF are interpreted by games and the terms by certain history-free strategies. This model is shown to capture definability in PCF. More precisely, every compact strategy in the model is definable in a certain simple extension of PCF. We then introduce an intrinsic preorder on strategies and show that it satisfies some striking properties such that the intrinsic preorder on function types coincides with the pointwise preorder. We then obtain an order-extensional fully abstract model of PCF by quotienting the intensional model by the intrinsic preorder. This is the first syntax-independent description of the fully abstract model for PCF. (Hyland and Ong have obtained very similar results by a somewhat different route, independently and at the same time. ) We then consider the effective version of our model and prove a universality theorem: every element of the effective extensional model is definable in PCF. Equivalently, every recursive strategy is definable up to observational equivalence. (C) 2000 Academic Press.

关键词： game semantics full abstraction sequentiality PCF functional computation programming language semantics linear logic

来源：评论

学校读者我要写书评

暂无评论

Modelling contextuality by probabilistic programs with hypergraph semantics

引用

THEORETICAL COMPUTER SCIENCE 2018年 752卷 56-70页

作者： Bruza, Peter D. Queensland Univ Technol Sch Informat Syst GPO Box 2434 Brisbane Qld 4001 Australia

Models of a phenomenon are often developed by examining it under different experimental conditions, or measurement contexts. The resultant probabilistic models assume that the underlying random variables, which define a measurable set of outcomes, can be defined independent of the measurement context. The phenomenon is deemed contextual when this assumption fails. Contextuality is an important issue in quantum physics. However, there has been growing speculation that it manifests outside the quantum realm with human cognition being a particularly prominent area of investigation. This article contributes the foundations of a probabilistic programming language that allows convenient exploration of contextuality in wide range of applications relevant to cognitive science and artificial intelligence. Using the style of syntax employed by the probabilistic programming language WebPPL, specific syntax is proposed to allow the specification of "measurement contexts". Each such context delivers a partial model of the phenomenon based on the associated experimental condition described by the measurement context. An important construct in the syntax determines if and how these partial models can be consistently combined into a single model of the phenomenon. The associated semantics are based on hypergraphs in two ways. Firstly, if the schema of random variables of the partial models is acyclic, a hypergraph approach from relational database theory is used to compute a join tree from which the partial models can be combined to form a single joint probability distribution. Secondly, if the schema is cyclic, measurement contexts are mapped to a hypergraph where edges correspond to sets of events denoting outcomes in measurement contexts. Recent theoretical results from the field of quantum physics show that contextuality can be equated with the possibility of constructing a probabilistic model on the resulting hypergraph. The use of hypergraphs opens the door for a theoreticall

关键词： Probabilistic programming Probabilistic modelling programming language semantics Contextuality

来源：评论

学校读者我要写书评

暂无评论

Scenario-Based Algorithmics: Coding Algorithms by Automatic Composition of Separate Concerns

引用

COMPUTER 2021年第10期54卷 95-101页

作者： Harel, David Marron, Assaf Yerushalmi, Raz Weizmann Inst Sci IL-76100 Rehovot Israel

A method for programming reactive systems, called scenario-based algorithmics, can have several advantages, both in programming and in computer science education. We provide new examples, experiments, and perspectives.

关键词： Formal Specification Functional programming programming language semantics Automatic Composition Separate Concerns programming Reactive Systems Called Scenario Based Algorithmics Computer Science Education Encoding Computer Science Education programming Profession

来源：评论

学校读者我要写书评

暂无评论

Latent semantic analysis of game models using LSTM

引用

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN programming 2019年 106卷 39-54页

作者： Ghica, Dan R. Alyahya, Khulood Univ Birmingham Birmingham W Midlands England Univ Exeter Exeter Devon England King Saud Univ Riyadh Saudi Arabia

We are proposing a method for identifying whether the observed behaviour of a function at an interface is consistent with the typical behaviour of a particular programming language. This is a challenging problem with significant potential applications such as in security (intrusion detection) or compiler optimisation (profiling). To represent behaviour we use game semantics, a powerful method of semantic analysis for programming languages. It gives mathematically accurate models ('fully abstract') for a wide variety of programming languages. Game-semantic models are combinatorial characterisations of all possible interactions between a term and its syntactic context. Because such interactions can be concretely represented as sets of sequences, it is possible to ask whether they can be learned from examples. Concretely, we are using LSTM, a technique which proved effective in learning natural languages for automatic translation and text synthesis, to learn game-semantic models of sequential and concurrent versions of Idealised Algol (IA), which are algorithmically complex yet can be concisely described. We will measure how accurate the learned models are as a function of the degree of the term and the number of free variables involved. Finally, we will show how to use the learned model to perform latent semantic analysis between concurrent and sequential Idealised Algol. (C) 2019 Elsevier Inc. All rights reserved.

关键词： programming language semantics Game semantics Recurrent neural networks Machine learning

来源：评论

学校读者我要写书评

暂无评论

Ontological approach for the semantic recovery of traceability links between software artefacts

引用

IET SOFTWARE 2008年第3期2卷 185-203页

作者： Zhang, Y. Witte, R. Rilling, J. Haarslev, V. Concordia Univ Dept Comp Sci & Software Engn Montreal PQ Canada

Traceability links provide support for software engineers in understanding relations and dependencies among software artefacts created during the software development process. The authors focus on re-establishing traceability links between existing source code and documentation to support software maintenance. They present a novel approach that addresses this issue by creating formal ontological representations for both documentation and source code artefacts. Their approach recovers traceability links at the semantic level, utilising structural and semantic information found in various software artefacts. These linked ontologies are supported by ontology reasoners to allow the inference of implicit relations among these software artefacts.

关键词： software development process semantic recovery inference mechanisms system documentation Diagnostic, testing, debugging and evaluating systems program diagnostics software artefact software engineer software maintenance programming language semantics ontologies (artificial intelligence) Software engineering techniques formal ontological representation Knowledge engineering techniques ontological reasoning software documentation traceability link Formal languages and computational linguistics

来源：评论

学校读者我要写书评

暂无评论

A LAYERED, OPERATIONAL MODEL OF DATA CONTROL IN programming-languageS

引用

COMPUTER languageS 1991年第2期16卷 147-165页

作者： OUDSHOORN, MJ MARLIN, CD UNIV ADELAIDE CTR COMP SYST & SOFTWARE ENGNADELAIDESA 5001AUSTRALIA

This paper describes a layered model of the semantics of the data control aspect of programming languages;this aspect of programming language semantics concerns access to the data objects of the program. The model is an information structure model in which the information structures are defined in a relatively precise manner using algebraic specification techniques for abstract data types. The use of abstract data types is also the key to the layering of the description: the outermost layer describes the semantics of the language feature, the middle layer contains definitions for the manipulation of the information structures used within the model, and the innermost layer contains precise descriptions of these information structures.

关键词： DATA CONTROL programming language semantics INFORMATION STRUCTURE MODELS PASCAL

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：