Deva(ID:1723/dev001)

Typed functional language with deduction rules, capable of specifying programa as well as types

Refer extract from Anlauff (1993) for summary

Computer Aided Formal Reasoning Group, Technical University Berlin

Structures:
Related languages
VDM-SL => Deva   Evolution of
References:
  • Weber, Matthias "Deriving Transivity of VDM-Reification in DEVA" VDM Europe (1) 1991: 406-427 view details
  • Anlauff, M. "Devil - Deva's Interactive Laboratory. Tutorial and user manual" Technical Report 93-42, TU Berlin, 1993. view details ps Abstract: Devil is a support tool for the development language Deva. Deva is a development language in which one may describe formal calculi underlying programming development methods and express formal proofs and developments. Devil provides an efficient support for Deva by several features such as an interactive user interface and theory compilation.

    The Devil system exists in a textual version for alphanumeric terminals and in a graphical version for X-Windows systems. This paper contains a description of the system - focusing on the graphical system - and its use. Extract: What is Deva?
    What is Deva?
    Deva is a generic language for formal development. "Generic" means, that you can instantiate Deva to many theories or methods by writing a Deva formalizations implementing the corresponding axioms and rules. After that, you can express developments on the basis of  this formalization; e.g. you can prove properties and derive more complex laws valid in your  theory. All these formalizations are carried out in one and the same framework; you need not  to switch between a notation for axioms and rules and one for proofs and developments.  In order to give you a chance to be able to read a Deva development, the main constructs will  be introduced first. Technically, Deva is based on a lambda-calculus with dependent types. There  exists a type hierarchy, the top element of which is called prim. A Deva development consists  of a list of contexts. In the simplest case a context is a variable binding introducing a new  Deva variable within a declaration or a definition. A declaration x :t introduces the variable  x to be of type t; a definition x :=t introduces x as an abbreviation for t. In both cases  we have bound a Deva text variable, and t stands for a valid Deva text. There exists also a  possibility to group a list of bindings; this is done within a context!definition context p:=c  which introduces p as an abbreviation of the context c which in general is a list of bindings.

    Each variable introduced by a variable binding can be used to build up valid Deva constructs in the subseqent development. The most important constructs of Deva texts are

    • the use of a text variable x;
    • the abstraction [c|-t] which can be seen as a formula t with local parameters introduced in the context c;
    • the application t1(t2), where t1 stands for an abstraction whose first parameter is instantiated to t2;
    • the judgement t1 :. t2 is an assertion, that t1 is of type t2
  • Biersack, M. ; R. Raschke, and M. Simons. The DevaWEB System: Introduction, Tutorial, User Manual, and Implementation. Technical Report 93-39, TU Berlin, 1993 view details Abstract: We focus on the literate and structured presentation of formal developments. We present an approach that is influenced by ideas from Leslie Lamport on how to write proofs, by Donald Knuth's paradigm of literate programming, and by the ideas of the "Dutch school'' on formal reasoning. We demonstrate this approach by presenting the proofs of two mathematical theorems --- the Knaster-Tarski fixpoint theorem and the Schr"oder-Bernstein theorem --- formalized in Deva. We discuss to what degree our aims have been achieved and what is left to be done.
    The report includes a tutorial on the use of the DevaWEB system and a user manual for that tool. Some remarks on the implementation which we hope are of general interest to the designer of language dependent WEB systems are also included.

    The report has been prepared with the assistance of the DevaWEB system and the Deva formalization has been checked by an implementation of Deva. ps
  • Simons, Martin; Lafontaine, Christine; Weber, Matthias K "The generic development language Deva: presentation and case studies". LNCS 738 Berlin Springer. view details Abstract: This book summarizes work done by the authors under the Esprit Tool Use project (1985-1990), at GMD in Karlsruhe and at Berlin University of Technology. It provides a comprehensive description of the generic development language Deva designed by the authors. Much of the research reported in this monograph is inspired by the work of Michel Sintzoff on formal program development; he contributed an enlightening Foreword. Deva is essentially a typed functional language with certain deduction rules. The difference with ordinary languages is, of course, the application domain: the types serve here to express propositions such as specifications or programs, rather than just data classes. Its practical applicability was tested on several non-trivial case studies. The whole book is written using the DVWEB system, a WEB for Deva, beeing implemented at the Berlin University of Technology.
  • Weber, Matthias "Definition and Basic Properties of the Deva Meta-Calculus" pp391-431 view details
          in Formal Aspects of Computing 5(5) 1993 view details
  • Beyer, M. ; S. Jähnichen, F. Kammüller, and T. Santen. Formalization of Algebraic Specification in the Development Language DEVA. In: M. Broy, S. Jähnichen (eds.). KORSO: Methods, Languages, and Tools for the Construction of Correct Software - Final Report. LCNS 1009, Springer-Verlag, 1995. view details
          in Formal Aspects of Computing 5(5) 1993 view details
  • Library of Congress Subject Headings D4 view details
          in Formal Aspects of Computing 5(5) 1993 view details