scholarly journals Unifying execution of imperative generators and declarative specifications

2020 ◽  
Vol 4 (OOPSLA) ◽  
pp. 1-26
Author(s):  
Pengyu Nie ◽  
Marinela Parovic ◽  
Zhiqiang Zang ◽  
Sarfraz Khurshid ◽  
Aleksandar Milicevic ◽  
...  
Keyword(s):  
Declarative Specifications

Verifying Web Site Properties Using Computational Logic

2003 ◽  
pp. 22-39
Author(s):  
Joao Cavalcanti ◽  
David Robertson
Keyword(s):  
Web Sites ◽  
Web Site ◽  
Integrity Constraint ◽  
Challenging Problem ◽  
Computational Logic ◽  
Constraint Specification ◽  
Specification And Verification ◽  
Natural Way ◽  
Design And Construction ◽  
Declarative Specifications

The continuing increase in size and complexity of Web sites has turned their design and construction into a challenging problem. Systematic approaches can bring many benefits to Web site construction, making development more methodical and maintenance less time consuming. Computational logic can be successfully used to tackle this problem, as it supports declarative specifications and reasoning about specifications in a more natural way. Computational logic also offers metaprogramming capabilities that can be used to develop methods for automated Web site synthesis. This chapter presents an approach to Web site synthesis based on computational logic and discusses in more detail two important features of the proposed approach: the support for property checking and integrity constraint specification and verification.

Translating Advanced Integrity Checking Technology to SQL

2002 ◽  
pp. 203-249 ◽  
Author(s):  
Hendrik Decker
Keyword(s):  
Natural Language ◽  
Order Logic ◽  
Predicate Calculus ◽  
Integrity Constraints ◽  
First Order Logic ◽  
First Order ◽  
Integrity Checking ◽  
Natural Language Interface ◽  
User Friendly ◽  
Declarative Specifications

The main goal of this chapter is to arrive at a coherent technology for deriving efficient SQL triggers from declarative specifications of arbitrary integrity constraints. The user may specify integrity constraints declaratively as closed queries in predicate calculus syntax (i.e., sentences in the language of first-order logic, abbr. FOL), as datalog denials, as query conditions in SQL WHERE clauses, or in some other, possibly more user-friendly manner (e.g., via a dialog-driven graphical or natural language interface which internally translates to equivalent WHERE clause conditions). As we are going to see, the triggers derived from such specifications behave such that whenever some update event would violate any of the integrity constraints, one or several of the triggers derived from that constraint are activated in order to enforce the constraint. That is, the violation is either prevented by rolling back the update or repaired instantly by subsequent further updates.

scholarly journals Recursive subtyping revealed

2002 ◽  
Vol 12 (6) ◽  
pp. 511-548 ◽  
Author(s):  
VLADIMIR GAPEYEV ◽  
MICHAEL Y. LEVIN ◽  
BENJAMIN C. PIERCE
Keyword(s):  
Programming Language ◽  
Efficient Implementation ◽  
Basic Theory ◽  
Mathematical Framework ◽  
Fundamental Theory ◽  
The Core ◽  
End To End ◽  
Declarative Specifications

Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they relate to simpler declarative specifications is not widely understood, due in part to the difficulty of the available introductions to the area. This tutorial paper offers an ‘end-to-end’ introduction to recursive types and subtyping algorithms, from basic theory to efficient implementation, set in the unifying mathematical framework of coinduction.

scholarly journals Declarative specifications

1996 ◽  
Vol 11 (4) ◽  
pp. 317-331 ◽  
Author(s):  
Norbert E. Fuchs ◽  
David Robertson
Keyword(s):  
Formal Specification ◽  
Domain Specificity ◽  
Formal Specifications ◽  
Application Domain ◽  
Specification Languages ◽  
Application Specific ◽  
Declarative Specifications

AbstractDeriving formal specifications from informal requirements is extremely difficult since one has to overcome the conceptual gap between an application domain and the domain of formal specification methods. To reduce this gap we introduce application-specific specification languages, i.e., graphical and textual notations that can be unambiguously mapped to formal specifications in a logic language. We describe a number of realised approaches based on this idea, and evaluate them with respect to their domain specificity vs. generality.

Sign in / Sign up

Export Citation Format

Share Document