HASLab  Indexed Articles in Journals
Permanent URI for this collection
Browse
Browsing HASLab  Indexed Articles in Journals by Author "5601"
Results Per Page
Sort Options

ItemComputer Aided Verification of Relational Models by Strategic Rewriting( 2017) Visser,J ; Uzal,R ; Necco,CM ; José Nuno Oliveira ; 5601Binary relational algebra provides semantic foundations for major areas of computing, such as database design, statebased modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations such as database queries, state transitions, or composition of functional components. When data models, their constraints and operations are represented by pointfree binary relational expressions, proof obligations can be expressed as inclusions between relational expressions. We developed a typedirected, strategic term rewriting system that can be used to simplify relational proof obligations and ultimately reduce them to tautologies. Such reductions can be used to provide extended static checking for design contraints commonly found in software modeling and development.

ItemProgramming from metaphorisms( 2018) José Nuno Oliveira ; 5601This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express inputoutput relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement studied in this paper is a strategy known as change of virtual data structure. By framing metaphorisms in the class of (inductive) regular relations, sufficient conditions are given for such implementations to be calculated using relation algebra. The strategy is illustrated with examples including the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.