Exploring the Effect of Control-Flow and Traversal Direction on VPL Usability for Novices

Programming is a hard cognitive activity, especially for novices who also have to struggle with learning the intricacies of the programming language syntax. We postulate that a well-designed diagrammatic visual programming language (VPL) to replace or substitute a textual programming language may help in the learning programming process. Our research focuses on the suitability of diagrammatic notations for such a VPL. In this paper, we report results from two experimental studies into diagrammatic notations. The first experiment shows the superiority of three visual representations over a conventional style textual program in both control- and data-flow paradigms. The result also shows the effect of programming paradigm on novices' performance. The second experiment focuses on two aspects of program flow representation: the graphical representation to be used for sequencing, and the traversal direction required of diagram users. It reveals that graphical representation does not affect performance in tracing program flow but that traversal direction makes a difference in cognitive demand on users. The evidence also indicates a control-flow preference among novices.     

Defining the abstract syntax of visual languages with advanced graph grammars—A case study based on behavior trees

Diagrammatic visual languages can increase the ability of engineers to model and understand complex systems. However, to effectively use visual models, the syntax and semantics of these languages should be defined precisely. Since most diagrammatic visual models that are currently used to specify systems can be described as (directed) typed graphs, graph grammars have been identified as a suitable formalism to describe the abstract syntax of visual modeling languages. In this article, we investigate how advanced graph-transformation techniques, such as conditional, structure-generic and type-generic graph-transformation rules, can help to improve and simplify the specification of the abstract syntax of a visual modeling language. To demonstrate the practicability of an approach that unifies these advanced graph-transformation techniques, we define the abstract syntax of behavior trees (BTs), a graphical specification language for functional requirements. Additionally, we provide a translational semantics of BTs by formalizing a translation scheme to the input language of the SAL model checking tool for each of the graph-transformation rules.     

Correct and Robust Programs

The design of programs which are both correct and robust is investigated. It is argued that the notion of an exception is a valuable tool for structuring the specification, design, verification, and modification of such programs. The syntax and semantics of a language with procedures and exception handling are presented. A deductive system is proposed for proving total correctness and robustness properties of programs written in this language. The system is both sound and complete. It supports proof modularization, in that it allows one to reason separately about fault-free and fault-tolerant system properties. Since the programming languages considered closely resembles CLU or Ada, the presented deductive system is easily adaptable for verifying total correctness and robustness properties of programs written in these, or similar, languages.     

The design of an interactive program development system for Pascal

A program language can be defined as the language in which computer programs are written, and a programming language as the language used by the programmer to create programs. This paper presents the design of an interactive program development system which uses Pascal as both program and programming language. Principal properties of the system are a complete immediate syntax check, a program-structure oriented editor, incremental compiling techniques, and interactive interpretation and debugging of programs. The syntax check is split into three phases, and the user can change the degree of check wanted. After a change of the program only part of it is recompiled, and only necessary phases of the compiling process are performed.     

Predicates and pixels

This paper explores the possibilities of programming with graphical representations of logic programs. Two example programs are given in the concurrent logic language FGDC but many languages based on rewrite rules would be suitable for the same treatment. A graphical syntax promises to make programming in suitable ultra high level languages easier and more intuitive.     

An operational formal definition of PROLOG: a specification method and its application

We present in this paper a logic programming specification language and its application to the formal specification of PROLOG dialects (Marseille-Edinburgh like dialect or parallel logic programs). In particular it is used in the standardization work of PROLOG. The specification language is based on normal clauses (definite clauses with possibly negative literals in the body) whose semantics is the set of the (generalized) proof-trees. We restrict the specification language to stratified programs and ground proof-trees such that its semantics fits with most of the usual known semantics in logic programming. The specification language is fully declarative in the sense that it is written in a pure logical stule. It is relatively easy to deduce an executable specification from a specification written in such a language. Part of the specification are the associated comments and a methodology has been developed to write these. Without the comments a formal specification cannot be understood; they are partly formal and serve only to help to understand the axioms. They are a natural language form of formal statements relative to the correctness and the completeness of the axioms with regards to some intended meaning. We show in this paper how this specification language can be used to specify dialects of PROLOG. The presented example is just a sample of PROLOG but fully developed here. The specification language has already been used for real dialects as PARLOG and standard PROLOG. This specification method is also interesting because it illustrates the power of logic programming to make specifications. It seems to us that logic programming is generally considered as “impure” executable specification. Our purpose is to show that logic programming may also be used as a perhaps low level but full specification language.     

Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application

The trip computers for the two reactor shutdown systems of the Ontario Power Generation (OPG) Darlington Nuclear Power Generating Station are being refurbished due to hardware obsolescence. For one of the systems, the general purpose computer originally used is being replaced by a programmable logic controller (PLC). The trip computer application software has been rewritten using function block diagrams (FBDs), a commonly used PLC programming language defined in the IEC 61131-3 standard. The replacement project’s quality assurance program requires that formal verification be performed to compare the FBDs against a formal software requirements specification written using tabular expressions (TEs). The PVS theorem proving tool is used in formal verification. Custom tools developed for OPG are used to translate TEs and FBDs into PVS code. In this paper, we present a method to rigorously translate the graphical FBD language to a mathematical model in PVS using an abstract syntax to represent the FBD constructs. We use an example from the replacement project to demonstrate the use of the model to translate a FBD module into a PVS specification. We then extend that example to demonstrate the method’s applicability to a Simulink-based design.     

NDAUTO：An Experimental Software Automation System

This paper describer the design and implementation of an experimental software automation system(NDAUTO).By combining the transformational and procedural approaches in software gutomation,the system can tansform software unctional specifications written in a graphical specification language GSPEC to executable programs sutomatically,The equivalence between a specification and its corresponding program can be guaranteed by the system,and the correctness of the specification can also be validated.The main new points of the work lie in the design of the specification languange,the transformation mechanism and the correctness validation of the specification.     

An architecture for processing graph-grammar applications

We propose a six-layer architecture for processing graph-grammar applications. The layers and the transformations between them are formally described and concepts for their implementation are given. Especially we introduce the syntax and semantics of a graph-grammar implementation language. Graph-grammar productions will be translated into programs of this language to have a basis for their implementation into programs written in commonly available programming languages.     

An agile approach to language modelling and development

We have developed novel techniques for component-based specification of programming languages. In our approach, the semantics of each fundamental programming construct is specified independently, using an inherently modular framework such that no reformulation is needed when constructs are combined. A language specification consists of an unrestricted context-free grammar for the syntax of programs, together with an analysis of each language construct in terms of fundamental constructs. An open-ended collection of fundamental constructs is currently being developed. When supported by appropriate tools, our techniques allow a more agile approach to the design, modelling, and implementation of programming and domain-specific languages. In particular, our approach encourages language designers to proceed incrementally, using prototype implementations generated from specifications to test tentative designs. The components of our specifications are independent and highly reusable, so initial language specifications can be rapidly produced, and can easily evolve in response to changing design decisions. In this paper, we outline our approach, and relate it to the practices and principles of agile modelling.     

SLAN-4?A Software Specification and Design Language

SLAN-4 (``Software Language-4') was developed to meet the need for a formal tool for specifying and designing large software systems. It provides language constructs for algebraic and axiomatic specifications and also pseudocode constructs for the design step. A major design goal was to ease subsequent refinements of a (given) specification. The design can start with a very informal specification, which can be implemented later using lower level concepts. This paper gives an overview of the SLAN-4 syntax and semantics. It concentrates on the most important aspects of: ? abstract data types, ? algebraic specification of abstract data types, and ? axiomatic specification of modules. Because the pseudocode part of SLAN-4 consists mainly of control structures similar to those in modern high-level programming languages, this element of the language is not separately described. The paper includes an example of how to use SLAN-4, and also the experiences gained in using the language to formally specify a real-world software product of about 18 000 lines of code written in an IBM internal high-level language.     

Concurrent programming in VISO

Concurrent programming is more difficult to use and understand than sequential programming. In order to simplify this type of programming a number of approaches have been developed such as visual programming. Visual Occam (VISO) is a visual programming language for concurrent programming. It has a graphical syntax based on the language Occam and its semantics is represented both in petri net and process calculus. This paper presents a modular visual approach to write concurrent programs using the VISO language. Concurrent programs in VISO are specified graphically at different levels of abstraction. This paper describes this modular visual approach by constructing two examples in VISO. The first example is a simple concurrent program and it is mainly used to show the details of constructing a concurrent program in VISO. The second example is a larger concurrent program with more levels of abstraction. Copyright © 2000 John Wiley & Sons, Ltd.     

A declarative coordination language

We describe Gammalog, a logic language whose semantics is based on the chemical metaphor. The language combines the ability of describing coordination by transformation rules on a shared-dataspace, as in Gamma, with the execution model of logic programming. The main feature of Gammalog is that the declarative reading of programs is not restricted to the pure logic language but it also includes the coordination mechanisms. This feature makes Gammalog a promising alternative to other coordination models which can be embedded in logic programming. We present the language syntax, its formal semantics, and a prototype implementation based on Gödel, which inherits its strongly typed framework. As an example of the expressive power of the language we provide the specification of a simple operating system.     

Language design for program manipulation

The design of procedural and object-oriented programming languages is considered with respect to how easily programs written in those languages can be formally manipulated. Current procedural languages such as Pascal, Modula-2 and Ada; generally support such program manipulations, except for some annoying anomalies and special cases. Three main areas of language design are identified as being of concern from a manipulation viewpoint: the interface between concrete and abstract syntax; the relationship between the abstract syntax and static semantics naming, scoping and typing; and the ability to express basic transformations (folding and unfolding). Design principles are suggested so that the problems identified for current languages can be avoided in the future     

Formatted syntaxes and modula-2

The formatted syntax notation has been developed for the specification of formatted programming languages. This paper describes how a formatted syntax may be constructed for the purpose of prettyprinting an existing free-format language. Those aspects of the system of particular relevance to free-format languages are emphasized and their use explained. Also, a number of deficiencies in the defining metasyntax and formatting symbol repertoire are discussed. Practical enhancements and further areas of research are suggested. The programming language Modula-2 is used for illustration, and a formatted syntax for it is given.     

XML-based Specification of Diagram Editors

This paper describes a graphical specification tool for Dia Gen, a diagram editor generator based on hypergraph grammars and hypergraph transformation. The specification tool greatly simplifies the process of specifying and generating diagram editors. It uses an XML-based specification language, and it is an extension of a generic XML editor which offers syntax-directed editing based on the DTD, i.e, syntax specification, of the underlying XML-based language.     

Automatic generation of visual programming environments

We have developed the visual language compiler-compiler (VLCC) system to automatically generate visual programming environments. VLCC is a grammar based system that can support implementation of any visual language by assisting the language designer in defining the language's graphical objects, syntax, and semantics. The final result of the generation process includes an integrated environment with a visual editor and a compiler for the defined visual language. In VLCC, graphical tools define visual languages to create both graphical objects and composition rules. Visual editors enable language designers to directly and visually manipulate the syntax of these languages. To capture the widest range of visual languages, the VLCC system can be configured for a specific language class. Different language classes can be characterized depending on their graphical objects' structure and on the way they can be composed. Also, box and arrow diagrams are defined for primitive objects with attaching points and for composition rules to join boxes and arrows at those attaching points. After choosing the visual language type to create, the designer can concentrate on language definition details. VLCC uses the positional grammar model as its underlying grammar formalism     

Agent规范与编程语言SPLAW的语法和语义

本文描述了Ａｇｅｎｔ规范与编程语言ＳＰＬＡＷ的语法，为ＳＰＬＡＷ中的各种语言成分提供了操作语义，并基于标记转换系统给出Ａｇｅｎｔ性质的证明规则。由于ＳＰＬＡＷ的通信部分采用不依赖于具体应用的Ａｇｅｎｔ交互语言ＫＱＭＬ，使遵循同一标准的Ａｇｅｎｔ之间能进行协作问题求解。ＳＰＬＡＷ首次为Ａｇｅｎｔ提供继承支持，使其可以实现具有面向对象特征的多线程系统。ＳＰＬＡＷ屏了为语言引入内部模态词的缺陷，试图从外