From Solution to Problem Spaces: Formal Methods in the Context of Model-Based Development and Domain-Specific Languages

2011 ◽  
Author(s):  
Bernhard Schatz
Keyword(s):  
Formal Methods ◽  
Domain Specific Languages ◽  
Domain Specific ◽  
Model Based

scholarly journals Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny

10.29007/5zjp ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
Sebastian Erdweg ◽  
Mira Mezini
Keyword(s):  
Formal Methods ◽  
Programming Language ◽  
Type System ◽  
Type Systems ◽  
Domain Specific Languages ◽  
Smt Solver ◽  
Domain Specific ◽  
Efficient Type

\noindent Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas~\cite{GreweErdwegWittmannMezini15} project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from specifications of type systems. To this end, we investigate how to best automate typical steps within type soundness proofs.\noindent In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP~\cite{Sutcliffe98} and calls Vampire~\cite{KovacsV13} on them, and secondly, the programming language Dafny~\cite{Leino2010}, which translates proof goals and specifications to the intermediate verification language Boogie 2~\cite{Leino2008} and calls the SMT solver Z3~\cite{DeMoura2008} on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.

scholarly journals Typing Textual Entities and M2T/T2M Transformations in a Model Management Environment

2010 ◽  
Vol 13 (1) ◽  
Author(s):  
Andrés Vignaga
Keyword(s):  
Global Model ◽  
Model Management ◽  
Model Transformations ◽  
Domain Specific Languages ◽  
Domain Specific ◽  
Model Based ◽  
Large Sets ◽  
Concrete Syntax ◽  
Transformation Problems

Global Model Management (GMM) is a model-based approach for managing large sets ofinterrelated heterogeneous and complex MDE artifacts. Such artifacts are usually representedas models, however as many Domain Specific Languages have a textual concrete syntax,GMM also supports textual entities and model-to-text/text-to-model transformations whichare projectors that bridge the MDE technical space and the Grammarware technical space. Asthe transformations supported by GMM are executable artifacts, typing is critical forpreventing type errors during execution. We proposed the cGMM calculus which formalizesthe notion of typing in GMM. In this work, we extend cGMM with new types and rules forsupporting textual entities and projectors. With such an extension, those artifacts mayparticipate in transformation compositions addressing larger transformation problems. Weillustrate the new constructs in the context of an interoperability case study.

scholarly journals Formal Methods Meet Domain Specific Languages

2005 ◽  
pp. 187-206 ◽  
Author(s):  
Jean-Paul Bodeveix ◽  
Mamoun Filali ◽  
Julia Lawall ◽  
Gilles Muller
Keyword(s):  
Formal Methods ◽  
Domain Specific Languages ◽  
Domain Specific

scholarly journals Contracts for domain-specific languages in Ruby

2015 ◽  
Vol 50 (2) ◽  
pp. 23-34
Author(s):  
T. Stephen Strickland ◽  
Brianna M. Ren ◽  
Jeffrey S. Foster
Keyword(s):  
Domain Specific Languages ◽  
Domain Specific

scholarly journals Macros for domain-specific languages

2020 ◽  
Vol 4 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Michael Ballantyne ◽  
Alexis King ◽  
Matthias Felleisen
Keyword(s):  
Domain Specific Languages ◽  
Domain Specific
Sign in / Sign up

Export Citation Format

Share Document