View Source Document

Chris Pressey.md

Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Formal Specification

Algebraic Specification

Early history of algebraic specification (ASF+SDF in a primitive form).

Language Prototyping: an Algebraic Specification Approach

ASF+SDF (proto-Maude), algebraic specification of languages. Contains an algebraic formulation of the lambda calculus as an example.

Several chapters unread which might have interesting things to say about origin tracking and error reporting in algebraic specification (i.e. this term that we rewrote to, where did it come from, what was its journey).

The Essence of Z

An introduction to the Z specification language.

Introduction to Z and Discrete Methods

Fairly good introduction to Z and writing specifications for programs. Includes a lot of introduction to the logical underpinnings as well.

Understanding Z

Formal denotational semantics of Z notation.

Program specification and transformation

This is more about program generation and (source-to-source) compiler techniques (a la partial evaluation) than about specification.

It's conference proceedings. One paper that might be worth reading in more detail is "Compile-time Garbage Collection" by Maurice Brutnooghe. But partly because I'm curious about the "functional language disguised as a logic programming language" defined therein.

"Distributive Laws for Composition and Union of Modules" also seems vaguely interesting. Also "Modal Logics for Applicative Programs" by Pepper.

Also contains "Two Exercises Found in a Book on Algorithmics" by Bird and Meertens, a (blurry) scan on which can be found here

Some transcribed discussions and speeches that might also be interesting to read.

Semantics, applications, and implementation of program generation

It's also conference proceedings.

"Accomplishments and Research Challenges in Meta-programming" might be good as an overview type perspective. None of the other papers look particularly interesting (no, not even "Integrating Partial Evaluators into Interpreters").

Actually "A Design Methodology for Functional Programs" might be a bit OK.

The role of formalism in system requirements (full version)

.

Consistency Checking of Functional Requirements

.

Consistency Checking in Requirements Analysis

.

Automated Consistency Checking of Requirements Specifications

.

Automatic program generation from specifications using PROLOG

.

Syntactic Theories in Practice

I read it a while ago.

Should really be under "Formal Semantics", not "Formal Specification", with the understanding that the former is a specialization of the latter, for programming languages.

"Syntactic theories" is one approach to formal semantics (and there are most definitely others).

The authors combine two operations involved in interpreting syntactic theories into one, optimizing the process.

I also wrote down "continuation-passing style" in my notes for this for some reason.

Notes on B. Meyer\'s \"On Formalism in Specifications\"

.

Bertrand Meyer's technology+ blog - Software engineering, programming methodology, languages, verification, general technology, publication culture, and more

.

Attempto Project

Attempto Controlled English is a formally-defined subset of English. As such it can be used to write a formal specification which is also generaly readable. More resources are available at the "Tools and Resources" link on this site.

About the Unified Modeling Language Specification Version 2.5.1

.

Systems modeling language - Wikipedia

.

SysML Open Source Project: What is SysML? Who created it?

.

SE 507 Algebraic Specifications

.

Developing an Iterative Program to Compute a Tail Recursive Function

.

Software Blueprints Web Pages

.