Abstract This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output 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.
This paper introduces the metaphorism pattern of relational specification and addresses how specification following this pattern can be refined into recursive programs. Metaphorisms express input-output 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 proposed in this paper is a strategy known as change of virtual data structure. It gives sufficient conditions for such implementations to be calculated using relation algebra and illustrates the strategy with the derivation of quicksort as example.
Faced with the need to quantify software (un)reliability in the presence of faults, the semantics of state-based systems is urged to evolve towards quantified (e.g. probabilistic) nondeterminism. When one is approaching such semantics from a categorical perspective, this inevitably calls for some technical elaboration, in a monadic setting.
This paper proposes that such an evolution be undertaken without sacrificing the simplicity of the original (qualitative) definitions, by keeping quantification implicit rather than explicit. The approach is a monad lifting strategy whereby, under some conditions, definitions can be preserved provided the semantics moves to another category.
The technique is illustrated by showing how to introduce probabilism in an existing software component calculus, by moving to a suitable category of matrices and using linear algebra in the reasoning.
The paper also addresses the problem of preserving monadic strength in the move from original to target (Kleisli) categories, a topic which bears relationship to recent studies in categorial physics.
Abstract In the trend towards tolerating hardware unreliability, accuracy is exchanged for cost savings. Running on less reliable machines, functionally correct code becomes risky and one needs to know how risk propagates so as to mitigate it. Risk estimation, however, seems to live outside the average programmer's technical competence and core practice. In this paper we propose that program design by source-to-source transformation be risk-aware in the sense of making probabilistic faults visible and supporting equational reasoning on the probabilistic behaviour of programs caused by faults. à la Bird-Moor algebra of programming. This paper studies, in particular, the propagation of faults across standard program transformation techniques known as tupling and fusion, enabling the fault of the whole to be expressed in terms of the faults of its parts.
Inspired by the relational algebra of data processing, this paper addresses the foundations of data analytical processing from a linear algebra perspective. The paper investigates, in particular, how aggregation operations such as cross tabulations and data cubes essential to quantitative analysis of data can be expressed solely in terms of matrix multiplication, transposition and the Khatri–Rao variant of the Kronecker product. The approach offers a basis for deriving an algebraic theory of data consolidation, handling the quantitative as well as qualitative sides of data science in a natural, elegant and typed way. It also shows potential for parallel analytical processing, as the parallelization theory of such matrix operations is well acknowledged.
Problem statements often resort to superlatives such as in the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting one particular such solution optimal in some sense (the hard part).
This report introduces a binary relational combinator which mirrors thi linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution. The framework encompasses re-factoring of results previously developed by by Bird and de Moor for greedy and dynamic programming, in away which makes them less technically involved and therefore easier to understand and play with.
This volume contains the proceedings of TFM2009, the Second International FME Conference on Teaching Formal Methods, organized by the Subgroup of Education of the Formal Methods Europe (FME) association. The conference took place as part of the first Formal Methods Week (FMWeek), held in Eind- hoven, The Netherlands, in November 2009.
TFM 2009 was a one-day forum in which to explore the successes and fail- ures of formal method (FM) education, and to promote cooperative projects to further education and training in FMs. The organizers gathered lecturers, teach- ers, and industrial partners to discuss their experience, present their pedagogical methodologies, and explore best practices.
The evolution from non-deterministic to weighted automata represents a shift from qual- itative to quantitative methods in computer science. The trend calls for a language able to reconcile quantitative reasoning with formal logic and set theory, which have for so many years supported qualitative reasoning. Such a lingua franca should be typed, poly- morphic, diagrammatic, calculational and easy to blend with conventional notation.
This paper puts forward typed linear algebra as a candidate notation for such a unifying role. This notation, which emerges from regarding matrices as morphisms of suitable categories, is put at work in describing weighted automata as coalgebras in such categories.
Some attention is paid to the interface between the index-free (categorial) language of matrix algebra and the corresponding index-wise, set-theoretic notation.
In the trend towards tolerating hardware unreliability, accuracy is exchanged for cost savings. Running on less reliable machines, "functionally correct" code becomes risky and one needs to know how risk propagates so as to mitigate it. Risk estimation, however, seems to live outside the average programmer's technical competence and core practice. In this paper we propose that risk be constructively handled in functional programming by (a) writing programs which may choose between expected and faulty behaviour, and by (b) reasoning about them in a linear algebra extension to standard, a la Bird-Moor algebra of programming. In particular, the propagation of faults across standard program transformation techniques known as tupling and fusion is calculated, enabling the fault of the whole to be expressed in terms of the faults of its parts.
Abstract algebra has the power to unify seemingly disparate theories once they are encoded into the same abstract formalism. This paper shows how a relation-algebraic rendering of both database dependency theory and Hoare programming logic purports one such unification, in spite of the latter being an algorithmic theory and the former a data theory. The approach equips relational data with \emph{functional types} and an associated type system which is useful for database operation type checking and optimization. The prospect of a generic, unified approach to both programming and data theories on top of libraries already available in automated deduction systems is envisaged.
Device miniaturization is pointing towards tolerating imperfect hardware provided it is “good enough”. Software design theories will have to face the impact of such a trend sooner or later.
A school of thought in software design is relational: it expresses specifications as relations and derives programs from specifications using relational algebra.
This paper proposes that linear algebra be adopted as an evolution of relational algebra able to cope with the quantification of the impact of imperfect hardware on (otherwise) reliable software.
The approach is illustrated by developing a monadic calculus for component oriented software construction with a probabilistic dimension quantifying (by linear algebra) the propagation of imperfect behaviour from lower to upper layers of software systems.
This paper presents a strategy for applying sampling techniques to relational databases, in the context of data quality auditing or decision support processes. Fuzzy cluster sampling is used to survey sets of records for correctness of business rules. Relational algebra estimators are presented as a data quality-auditing tool.
This paper presents a survey of Formal Methods courses in European higher education carried out by the FME Subgroup on Education over the last two years. The survey data sample is made of 117 courses spreading over 58 higher-education institutions across 13 European countries and involving (at least) 91 academic staff.
A total number of 365 websites have been browsed which are accessible from the electronic (HTML) version of this paper in the form of links to course websites, lecturers and topic entries in encyclopedias or virtual libraries.Three main projections of our sample are briefly analysed. Although far from being fully representative, these already provide some useful indicators about the impact of formal methods in European computing curricula.
This paper sketches a discipline for reverse engineering which combines formal and semi-formal methods. Among the former is the "algebra of programming", which we apply in "reverse order" so as to reconstruct formal specifications of legacy code. The latter includes code slicing, used as a means of trimming down the complexity of handling the formal semantics of all program variables at the same time. A strong point of the approach is its constructive style. Reverse calculations go as far as imploding auxiliary variables, introducing mutual recursion (if applicable) and transforming semantic functions into standard generic programming schemata such as cata/paramorphisms. We illustrate the approach by reversing a piece of code (from C to Haskell) already studied in the code-slicing literature: the word-count (wc) program.
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming.The derivation of fusion, cancellation and abide laws from the biproduct equations makes it easy to calculate algorithms implementing matrixmultiplication, the kernel operation of matrix algebra, ranging from its divide-and-conquer version to the conventional, iterative one. From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
