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

A decision procedure for a decidable fragment of generalized constraint diagrams

JOURNAL OF VISUAL LANGUAGES AND COMPUTING 2011年第1期22卷 90-105页

作者： Burton, Jim Stapleton, Gem Hamie, Ali Univ Brighton Visual Modelling Grp Brighton BN2 4AT E Sussex England

constraint diagrams were introduced by Kent, in 1997, as an alternative to the OCL for placing formal constraints on software models. Since their introduction, constraint diagrams have evolved and, after a careful analysis of their positive and negative features, generalized constraint diagrams were proposed. An important benefit of providing a formal model of a software system (diagrammatically or otherwise) is the ability to determine whether that model is consistent (i.e. satisfiable). However, determining satisfiability in an algorithmic, terminating, way is only possible in decidable logics. In this paper, we consider the so-called unitary existential fragment (UEF) of generalized constraint diagrams and, within this fragment, identify a decision procedure for the satisfiability of a particular class of diagrams. We then demonstrate how to extend the decision procedure to the UEF as a whole. This work lays the foundations for providing decision procedures for larger fragments of generalized constraint diagrams and we discuss how this might be achieved in the paper. (C) 2010 Elsevier Ltd. All rights reserved.

关键词： constraint diagrams Consistency Visual logic Formal diagrammatic reasoning

来源：评论

学校读者我要写书评

暂无评论

The semantics of augmented constraint diagrams

引用

JOURNAL OF VISUAL LANGUAGES AND COMPUTING 2005年第6期16卷 541-573页

作者： Fish, A Flower, J Howse, J Univ Brighton Visual Modelling Grp Brighton E Sussex England

constraint diagrams are a diagrammatic notation which may be used to express logical constraints. They generalize Venn diagrams and Euler circles, and include syntax for quantification and navigation of relations. The notation was designed to complement the Unified Modelling Language in the development of software systems. Since symbols representing quantification in a diagrammatic language can be naturally ordered in multiple ways, some constraint diagrams have more than one intuitive meaning I'll first-order predicate logic. Any equally expressive notation which is based oil Euler diagrams and conveys logical statements using explicit quantification will have to address this problem. We explicitly augment constraint diagrams with reading trees, which provides a partial ordering for the quantifiers (determining their scope as well as their relative ordering). Alternative approaches using spatial arrangements of components, or alphabetical ordering of symbols, for example, call be seen as implicit representations of a reading tree. Whether the reading tree accompanies the diagram explicitly (optimizing expressiveness) or implicitly (simplifying diagram syntax), we show how to construct unambiguous semantics for the augmented constraint diagram. (c) 2005 Elsevier Ltd. All rights reserved.

关键词： visual formalisms software specification formal methods constraint diagrams

来源：评论

学校读者我要写书评

暂无评论

Evaluating and generalizing constraint diagrams

引用

JOURNAL OF VISUAL LANGUAGES AND COMPUTING 2008年第4期19卷 499-521页

作者： Stapleton, Gem Delaney, Aidan Univ Brighton Visual Modelling Grp Brighton E Sussex England

The constraint diagram language was designed to be used in conjunction with the unified modelling language (UML), primarily for placing formal constraints on software models. In particular, constraint diagrams play a similar role to the textual object constraint language (OCL) in that they can be used for specifying system invariants and operation contracts in the context of a UML model. Unlike the OCL, however, constraint diagrams can be used independently of the UML. In this paper, we illustrate a range of intuitive and counter-intuitive features of constraint diagrams and highlight some (potential) expressiveness limitations. The counter-intuitive features are related to how the individual pieces of syntax interact. A generalized version of the constraint diagram language that overcomes the illustrated counter-intuitive features and limitations is proposed. In order to discourage specification readers and writers from overlooking certain semantic information, the generalized notation allows this information to be expressed more explicitly than in the non-generalized case. The design of the generalized notation takes into account five language design principles which are discussed in the paper. We provide a formalization of the syntax and semantics for generalized constraint diagrams. Moreover, we establish a lower bound on the expressiveness of the generalized notation and show that they are at least as expressive as constraint diagrams. (C) 2008 Elsevier Ltd. All rights reserved.

关键词： constraint diagrams precise software specification diagrammatic specification expressiveness

来源：评论

学校读者我要写书评

暂无评论

An experimental study into the default reading of constraint diagrams

An experimental study into the default reading of constraint...

引用

IEEE Symposium on Visual Languages and Human-Centric Computing

作者： Fish, A Masthoff, J Univ Brighton Brighton BN2 4AT E Sussex England

ISBN: (纸本)0769524435

constraint diagrams (Kent, 1997) are a complex diagrammatic notation designed to express logical statements especially for use in software specification and reasoning. Not surprisingly, since this is an expressive language, there are some difficulties in reading the semantics of a diagram unambiguously. Some extra annotations (in the form of a reading tree) disambiguate the diagrams. However, this extra requirement (of drawing a reading tree) places a burden on the user. An attempt to remove the need for such a reading tree (or perhaps to automatically generate a reading tree, which could be altered by a user if they wished to) has been given via an algorithm to generate a default reading from the diagram. This algorithm is based on a number of principles - most of which are properties of the diagram. We wish to know whether these principles are intuitive and whether the default reading reflects a good proportion of users' intuitions, and we have performed a user-based study to test this.

关键词： formal specification programming language semantics constraint diagrams diagrammatic notation logical statement reading tree software reasoning software specification

来源：评论

学校读者我要写书评

暂无评论

A reading algorithm for constraint diagrams

A reading algorithm for constraint diagrams

引用

IEEE Symposium on Human Centric Computing Languages and Environments

作者： Fish, A Flower, J Howse, J Univ Brighton Visual Modelling Grp Brighton BN2 4GJ E Sussex England

ISBN: (纸本)0780382250

constraint diagrams are a visual notation designed to complement the Unified Modeling Language in the development of software systems. They generalize Venn diagrams and Euler circles, and include facilities for quantification and navigation of relations. Their design emphasizes scalability and expressiveness while retaining intuitiveness. The formalization of constraint diagrams is non-trivial: previous attempts have exposed subtleties concerned with the ordering of symbols in the visual language. Consequently, some constraint diagrams have more than one intuitive reading. We develop the concept of the dependence graph for a constraint diagram. From the dependence graph we obtain a set of reading trees. A reading tree provides a partial ordering for some syntactic elements of the diagram. Given a reading tree for a constraint diagram, we present an algorithm that delivers a unique semantic reading.

关键词： visual formalisms software specification formal methods constraint diagrams diagrammatic reasoning

来源：评论

学校读者我要写书评

暂无评论

Towards a default reading for constraint diagrams

Towards a default reading for constraint diagrams

引用

3rd International Conference on diagrams

作者： Fish, A Howse, J Univ Brighton Visual Modeling Grp Brighton E Sussex England

ISBN: (纸本)354021268X

constraint diagrams are a diagrammatic notation which may be used to express logical constraints. They were designed to complement the Unified Modeling Language in the development of software systems. They generalize Venn diagrams and Euler circles, and include facilities for quantification and navigation of relations. Due to the lack of a linear ordering of symbols inherent in a diagrammatic language which expresses logical statements, some constraint diagrams have more than one intuitive meaning. We generalize, from an example based approach, to suggest a default reading for constraint diagrams. This reading is usually unique, but may require a small number of simple user choices.

关键词： visual formalisms diagrammatic reasoning software specification formal methods constraint diagrams

来源：评论

学校读者我要写书评

暂无评论

Investigating Reasoning with constraint diagrams

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2005年第4期127卷 53-69页

作者： Fish, Andrew Flower, Jean Univ Brighton Visual Modelling Grp Brighton BN2 4GJ E Sussex England

constraint diagrams are a visual notation designed to express logical constraints. Augmenting the diagrams with a reading tree (effectively a partial ordering of quantifiers) ensures that each diagram has a unique semantic interpretation. In this paper, we discuss examples of reasoning rules for augmented constraint diagrams which exhibit interesting properties or difficulties that can arise when developing rules for such a diagrammatic system. We do not present a complete set of rules, but investigate the generic problems arising, providing solutions. One problem corresponds to the nesting of quantifiers and another relates to the domain of universal quantification. These issues may be an important consideration in the definition of other logical reasoning systems which explicitly represent quantification diagrammatically.

关键词： Diagrammatic reasoning constraint diagrams logical inference

来源：评论

学校读者我要写书评

暂无评论

Diagrammatic Formal Specification of a Configuration Control Platform

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2009年第C期259卷 87-104页

作者： Howse, John Schuman, Steve Stapleton, Gem Oliver, Ian Univ Brighton Brighton E Sussex England Nokia Res Espoo Finland

This paper presents a diagrammatic logic framework that is suitable for use in formal specification and for reasoning about and refining formal software models. We take a case study style approach to presenting the framework by developing, in some detail, an abstract model for a transparent configuration control platform. The model is built up by stages, corresponding to separate concerns of configuration control. Each successive level is a refinement of the previous level. We discuss the possibilities for developing tools to support the use of the diagrammatic logic, including automated diagram drawing and reasoning procedures. Our wider goal is to make a formal specification easier for its clients to understand.

关键词： configuration control case-study constraint diagrams object-oriented formal specification visual modeling visual refinement

来源：评论

学校读者我要写书评

暂无评论

A diagrammatic reasoning system for the description logic ALC

引用

JOURNAL OF VISUAL LANGUAGES AND COMPUTING 2008年第5期19卷 539-573页

作者： Dau, Frithjof Eklund, Peter Univ Wollongong Wollongong NSW Australia

Diagrammatic reasoning is a tradition of visual logic that allows sentences that are equivalent to first order logic to be written in a visual or structural form: usually for improved usability. A calculus for the diagram can then be defined that allows well-formed formulas to be derived. This calculus is intended in the analog of logical inference. Description logics (DLs) have become a popular knowledge representation and processing language. DLs correspond to decidable fragments of first order logic;their notation is in the style of symbolic, variable-free formulas. Moreover, DLs are equipped with table au theorem provers that are proven to be sound and complete. Although DLs have roots in diagrammatic languages (such as semantic networks), they are elaborated in a purely symbolic manner. This paper discusses how DLs can be equivalently represented in terms of a diagrammatic reasoning system. First, existing diagrammatic reasoning systems, namely spider- and constraint diagrams, as well as existential and conceptual graphs, are investigated to determine if they are compatible with DLs. It turns out that Peirce's existential graphs are better suited for this purpose than the alternatives we examine. The paper then redevelops the DL ALC, which is the smallest propositional DL, by means of labeled trees, and provides a diagrammatic representation for these trees in the style of Peircean graphs. We provide a calculus based on C.S. Peirce's calculus for existential graphs and prove the soundness and completeness of the calculus. The calculus acts on labeled trees, but can be best understood as a diagrammatic calculus whose rules modify the Peircean-style representation of ALC. (C) 2008 Elsevier Ltd. All rights reserved.

关键词： description logics spider diagrams constraint diagrams conceptual graphs existential graphs logic syntax semantics calculus

来源：评论

学校读者我要写书评

暂无评论

Suitability of Visual Modelling Languages for Modelling Tangible User Interface Applications

Suitability of Visual Modelling Languages for Modelling Tang...

引用

IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC)

作者： Tobias, Eric Ras, Eric Amalio, Nuno Publ Res Ctr Henri Tudor Serv Sci JF Kennedy Av 29 L-1855 Luxembourg Luxembourg Univ Luxembourg Fac Sci Technol & Commun L-1359 Luxembourg Luxembourg

ISBN: (纸本)9781467308502

This paper compares the suitability of visual modelling languages for describing tangible user interface (TUI) applications. After gathering different approaches, we have selected three languages for our comparative study: the visual object constraint language (VOCL), augmented constraint diagrams (ACD), and the visual contract language (VCL). A weighted evaluation based on multiple quality criteria led to the conclusion that VCL is best suited to model TUI applications.

关键词： Visual Languages Model Driven Development Comparative Study VOCL constraint diagrams VCL

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：