about summary refs log tree commit diff stats
path: root/doc
diff options
context:
space:
mode:
authorDarren Bane <dbane@tilde.institute>2020-05-20 23:10:28 +0100
committerDarren Bane <dbane@tilde.institute>2020-05-20 23:10:28 +0100
commit01c8c655f67f820bc8028d369c5061c997921e72 (patch)
tree2b42b5838aa05ecbf2223abec31ba6a4d977dd70 /doc
parent020601c63c8878f82a06d597ae80de94295ef73d (diff)
downloadlsp-01c8c655f67f820bc8028d369c5061c997921e72.tar.gz
Blog post generator
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile19
-rw-r--r--doc/breaking_rules.md136
-rw-r--r--doc/refs1015
3 files changed, 1170 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
index 0000000..fa8d38d
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,19 @@
+.POSIX:
+.DELETE_ON_ERROR:
+
+.PHONY: all
+all: breaking_rules.pdf breaking_rules.html
+
+# Stick with gfm for as long as possible.
+# Use stuff beyond that only where absolutely necessary.
+# Similar to code, YAGNI.
+
+breaking_rules.pdf: breaking_rules.md refs
+	lowdown -sTms breaking_rules.md | pdfroff -i -t -R -mspdf -k -Kutf8 > $@
+
+breaking_rules.html: breaking_rules.md refs
+	lowdown -sTms breaking_rules.md | groff -Thtml -i -t -R -ms -k -Kutf8 > $@
+
+.PHONY: clean
+clean:
+	$(RM) breaking_rules.pdf
diff --git a/doc/breaking_rules.md b/doc/breaking_rules.md
new file mode 100644
index 0000000..aa3cb89
--- /dev/null
+++ b/doc/breaking_rules.md
@@ -0,0 +1,136 @@
+title: Breaking the Rules: Refining Prototypes Into Products  
+author: Darren Bane  
+copyright: 2020 Darren Bane, CC BY-SA  
+
+# Abstract
+
+Recommendations for a process to refine prototypes into production-quality code
+are made.
+\.R1
+accumulate
+\.R2
+
+# Introduction
+
+The conventional wisdom is that prototypes should be discarded once the lessons
+have been learned,
+and the final product written again from scratch.
+In the spirit of
+\.[
+beck 1999
+\.]
+I argue that improvements in development tools have
+invalidated this.
+
+*Colophon*: this document tries to depend only on GFM,
+in the same spirit as the software.
+The use of tools like
+PP, PlantUML and Pandoc is postponed indefinitely.
+
+# Literature Review
+
+There is a long history of recommending prototyping as a way to construct
+systems.
+I would personally recommend
+\.[
+robertson agust\(i 1999
+\.]
+and
+\.[
+pitman 1994
+\.]
+.
+
+A closely related are is that of "specification animation",
+quickly writing an implementation of some subset of a formal specification in
+for example Z or VDM.
+Prolog is a common choice for this, but I choose Lisp instead.
+
+However, as stated in the introduction, this document differs from these in
+arguing that it is possible to *refine* a prototype into a product.
+
+# Prototyping
+
+The first step is to construct a prototype,
+or in modern terminology a "Minimal Viable Product".
+These recommendations follow on from
+\.[
+robertson agust\(i 1999
+\.]
+and
+\.[
+bane 2008
+\.]
+.
+
+Reasons for choosing ISLisp include:
+
+* Procedural and object-oriented programming is commonly taught.
+  And seems to be easier to learn.
+* A disregard for popularity (which Common Lisp, or Java would win).
+  In fact, the language seems more popular in France and Japan than
+  the USA.
+* The efficiency gain from an integrated environment.
+  With Emacs and JSON-RPC it's not totally integrated, but is close.
+  ELisp and ISLisp are not identical but are very similar.
+* Contrary to a lot of other languages, it is fairly paradigm-agnostic.
+
+Unlike Prolog,
+users may end up writing logic eventually for DbC
+but there is no need to force it at the start.
+
+A JSON-RPC library was not difficult to write.
+
+## Imperative/Object-oriented paradigm
+
+Here, the following technology is recommended:
+
+* The OpenLisp interpreter.
+* Emacs for the view layer
+* JSON-RPC for inter-process communication
+
+Even though this is a prototype, attention should be paid to basic craftsmanship:
+
+* Divide the system into packages, using at least the subset of CL that is
+  supported by OpenLisp
+* Write one-sentence comments for at least each public fun and class
+* Use `assure`
+  to check the types of parameters in public interfaces
+* Some minimal documentation, at least an overview README file and man pages.
+
+### Further work
+
+This is probably the most work that makes sense
+without earning money.
+
+* Write contracts for public funs & classes
+* Could do simple multi-user,
+  using the IRCv3 bots (nickserv, chanserv) and IRCCloud or similar
+
+# Refinement to Production-Quality
+
+I argue that there is a repeatable procedure to improve the quality of a
+(reasonably well-written) prototype to a releaseable product.
+
+First, ensure that the surrounding infrastructure is in place:
+
+* Configuration management. The prototype should already have been checked into git.
+* Build. TODO: Read the recommendations in the OpenLisp manual?
+* Test.
+  Write olunit
+  test cases for any scenarios that aren't coverered by DbC.
+* Track. Start using a defect tracking system.
+
+Then, the following code & documentation improvements should be made:
+
+* Document the system more exhaustively
+* Port some of the trivial-\* CL libraries from quicklisp where justified.
+* Port to core-lisp on platform.sh?
+
+# Conclusion
+
+A method for developing software from an incomplete understanding of the requirements is given.
+It is hoped that this is more effective than most of what is currently-used.
+\.[
+$LIST$
+\.]
diff --git a/doc/refs b/doc/refs
new file mode 100644
index 0000000..5d000ea
--- /dev/null
+++ b/doc/refs
@@ -0,0 +1,1015 @@
+%A Ruth Abraham
+%T Evaluating Generalized Tabular Expressions in Software Documentation
+%R Tech. Rep. CRL 346
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D Feb 1997
+%K abr97
+
+%A Dennis Keith Peters
+%T Generating a Test Oracle from Program Documentation
+%R Tech. Rep. CRL 302
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D Apr 1995
+
+%A Constance L. Heitmeyer
+%T Software Cost Reduction
+%B Encyclopedia of Software Engineering
+%E John J. Marciniak
+%D Jan 2002
+%K hei02
+
+%A Constance L. Heitmeyer
+%A Myla Archer
+%A Ramesh Bharadwaj
+%A Ralph Jeffords
+%T Tools for constructing requirements specifications: The SCR toolset at the age of ten
+%J International Journal of Computer Systems Science & Engineering
+%V 20
+%N 1
+%P 19-35
+%D Jan 2005
+
+%A Constance L. Heitmeyer
+%A Ralph D. Jeffords
+%A Bruce G. Labaw
+%T Automated Consistence Checking of Requirements Specifications
+%J ACM Transactions on Software Engineering and Methodology
+%V 5
+%N 3
+%P 231-261
+%D Jul 1996
+
+%A A. J. Wilder
+%T Recursive Tables and Effective Definition Schemes
+%R Tech. Rep. CSR 11-99
+%I University of Wales Swansea
+%C Swansea, UK
+%D 1999
+
+%A Kathryn Heninger
+%T Specifying Software Requirements for Complex Systems: New Techniques and Their Application
+%J IEEE Transactions on Software Engineering
+%V 6
+%P 2-13
+%D 1980
+%K hen80
+
+%A Kathryn Heninger
+%A J. Kallander
+%A David L. Parnas
+%A John Shore
+%T Software Requirements for the A-7E Aircraft
+%R Memo Rep. 3876
+%I Naval Res. Lab.
+%C Washington, DC, USA
+%D 27 Nov 1978
+
+%A Ryszard Janicki
+%T Towards a formal semantics of Parnas tables
+%B Proceedings of the 17th International Conference on Software Engineering
+%P 231-240
+%D 1995
+
+%A Ryszard Janicki
+%T On a Formal Semantics of Tabular Expressions
+%R Tech. Rep. CRL 355
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 1997
+%K jan97
+
+%A Adam Balaban
+%A Darren Bane
+%A Ying Jin
+%A David Parnas
+%T Mathematical Model of Tabular Expressions
+%R Tech. Rep.
+%I University of Limerick
+%C Ireland
+%D 2007
+%K jbp04
+
+%A David L. Parnas
+%T Tabular Representation of Relations
+%R Tech. Rep. CRL 260
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 1992
+%K par92
+
+%A Ryszard Janicki
+%A David L. Parnas
+%A J. Zucker
+%T Tabular Representations in Relational Documents
+%B Relational Methods in Computer Science
+%E C. Brink
+%E G. Schmidt
+%I Springer Verlag
+%D 1977
+%P 184-196
+%O Reprinted in \fISoftware Fundamentals: Collected Papers by David L. Parnas\fP, D. M. Hoffman, D. M. Weiss, eds., Addison-Wesley
+
+%Q Software Engineering Research Group
+%T Table Tool System Developer's Guide
+%R Tech. Rep. CRL 339 & 340
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 1997
+%K serg97
+
+%A Tian Fu
+%T Structured Decision Table <=> Generalised Decision Table Conversion Tool
+%R Tech. Rep. CRL 380
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 1999
+%K fu99
+
+%A Markus Clermont
+%T Implementing the TTS Kernel with Excel
+%D 2005
+%K cle05
+
+%A Alan Wassyng
+%A Mark Lawford
+%T Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project
+%B FME2003: International Symposium of Formal Methods Europe Proceedings
+%C Pisa, Italy
+%D Sep 2003
+%P 133-153
+
+%A Herbert Sutter
+%T Exceptional C++
+%I Addison-Wesley
+%D 2000
+%K sut00
+
+%A Erik Meijer
+%A Maarten Fokkinga
+%A Ross Patterson
+%T Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
+%B FPCA91: Functional Programming Languages and Computer Architecture
+%E J. Hughes
+%V 523
+%S Lecture Notes in Computer Science (LNCS)
+%I Springer-Verlag
+%D Aug 1991
+%P 124-144
+%K mfp91
+
+%A David Schmidt
+%T Denotational Semantics: A Methodology for Language Development
+%I Allyn and Bacon
+%D 1986
+%K sch86
+
+%A Leslie Lamport
+%A Lawrence C. Paulson
+%T Should Your Specification Language be Typed?
+%R Research Report 147
+%I Digital Systems Research Center
+%C CA, USA
+%D 1997
+%K lp97
+
+%A Luca Cardelli
+%T Type Systems
+%B Handbook of Computer Science and Engineering
+%I CRC Press
+%D 1997
+%K car97
+
+%A Hong Shen
+%T Implementation of Table Inversion Algorithms
+%R Tech. Rep. CRL 315
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 1995
+%K she95
+
+%A Jeffery I. Zucker
+%A Hong Shen
+%T Table transformation: Theory and tools
+%R Tech. Rep. CRL 363
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 1998
+
+%A Stephen Eriksson-Bique
+%T A New Calculus for Multidimensional Arrays
+%B Proceedings of the 2002 Conference on APL: Array Processing Languages: Lore, Problems and Applications
+%I ACM Press
+%C Madrid, Spain and New York, NY, USA
+%D 2002
+%P 92-99
+%K eri02
+
+%A Paul R. Halmos
+%T Naive Set Theory
+%I Springer Verlag
+%D 1987
+%K hal87
+
+%A David L. Parnas
+%T Predicate Logic for Software Engineering
+%J IEEE Transactions on Software Engineering
+%V 19
+%N 9
+%P 856-862
+%O Reprinted in \fISoftware Fundamentals: Collected Papers by David L. Parnas\fP, D. M. Hoffman, D. M. Weiss, eds., Addison-Wesley
+%D 1993
+%K par93
+
+%A Min Jing
+%T A Table Checking Tool
+%R Tech. Rep. SERG 384
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 2000
+%K jin00
+
+%A Elliot Mendelson
+%T Introduction to Mathematical Logic, 3rd ed.
+%I Wadsworth & Brooks/Cole
+%D 1987
+%K men87
+
+%A David L. Parnas
+%A John E. Shore
+%A David Weiss
+%T Abstract Types Defined as Classes of Variables
+%B Proceedings of Conference on Data Abstraction, Definition and Structure
+%C Salt Lake City, USA
+%D Mar 1976
+%K psw76
+
+%A David L. Parnas
+%T Designing Software for Ease of Extension and Contraction
+%J IEEE Transactions on Software Engineering
+%P 128-138
+%O Reprinted in \fISoftware Fundamentals: Collected Papers by David L. Parnas\fP, D. M. Hoffman, D. M. Weiss, eds., Addison-Wesley
+%D 1979
+%K par79
+
+%A David L. Parnas
+%A Paul C. Clements
+%T A Rational Design Process and How to Fake it
+%J IEEE Transactions on Software Engineering
+%V 12
+%N 2
+%P 251-257
+%D Feb 1986
+
+%A William M. Farmer
+%T A Basic Extended Simple Type Theory
+%R Tech. Rep. SQRL 14
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 2003
+%K far03
+
+%A Hong Duan
+%T A Comparative Study of Pre/Postcondition and Relational Approaches to Program Development
+%R Tech. Rep. SQRL 24
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D Dec 2004
+
+%A Simon L. Peyton Jones, (ed)
+%T Haskell 98 Language and Libraries, the Revised Report
+%D Dec 2002
+%K pey02
+
+%A Sam Owre
+%A Natarajan Shankar
+%T The Formal Semantics of PVS
+%R Tech. Rep. CSL-97-2R
+%I SRI International Computer Science Laboratory
+%C USA
+%D 1999
+%K os99
+
+%A Sam Owre
+%A John M. Rushby
+%A Natarajan Shankar
+%T PVS: A Prototype Verification System
+%B Proceedings of the 11th International Conference on Automated Deduction (CADE)
+%C Saratoga, NY, USA
+%D 1992
+%P 748-752
+%E Deepak Kapur
+%S Lecture Notes in Artificial Intelligence
+%I Springer Verlag
+%V 607
+
+%A Ramesh Bharadwaj
+%A Steve Sims
+%T Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking
+%B Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
+%D 2000
+%S Lecture Notes in Computer Science
+%I Springer
+
+%A Myla Archer
+%A Constance L. Heitmeyer
+%A Elvinia Riccobene
+%T Proving Invariants of I/O Automata with TAME
+%J Automated Software Engineering
+%V 9
+%N 3
+%P 201-232
+%D 2002
+
+%A William M. Farmer
+%A Joshua D. Guttman
+%A F. Javier Thayer
+%T The Iota Constructor
+%B The IMPS User's Manual
+%D Apr 1995
+%K fgt95
+
+%A James H. Davenport
+%T A Small OpenMath Type System
+%I The OpenMath Consortium
+%D 1999
+%K dav99
+
+%A O. Caprotti
+%A A. M. Cohen
+%T A Type System for OpenMath
+%I The OpenMath Consortium
+%D 1999
+
+%A Harold Abelson
+%A Gerald J. Sussman
+%T Structure and Interpretation of Computer Programs, 2nd ed.
+%I The MIT Press
+%C MA, USA
+%D 1996
+%K sicp96
+
+%T X(7) On-Line Manual Page
+%I X Consortium, Inc.
+%D 2003
+%K xwin03
+
+%A David L. Parnas
+%A Paul C. Clements
+%A David M. Weiss
+%T The Modular Structure of Complex Systems
+%J IEEE Transactions on Software Engineering
+%V 11
+%N 3
+%P 251-257
+%O Reprinted in \fISoftware Fundamentals: Collected Papers by David L. Parnas\fP, D. M. Hoffman, D. M. Weiss, eds., Addison-Wesley
+%D 1985
+%K pcw85
+
+%A Bart Jacobs
+%T Categorical Logic and Type Theory
+%I Elsevier
+%C Amsterdam, The Netherlands
+%D 1985
+%K jac85
+
+%A Fred Brooks
+%T The Mythical Man-Month: Essays on Software Engineering
+%I Addison-Wesley
+%D 1975
+%K bro75
+
+%A Darren Bane
+%A Ying Jin
+%T Applicability System for Expressions, (working paper)
+%I University of Limerick
+%C Ireland
+%D 2004
+%K bj04
+
+%A Ying Jin
+%A David L. Parnas
+%T Scope Rules for Tabular Expressions, (working paper)
+%I University of Limerick
+%C Ireland
+%D 30 Sep 2004
+%K jp04
+
+%A Fairouz Kamareddine
+%A Rob Nederpelt
+%T A refinement of de Bruijn's formal language of mathematics
+%J Journal of Logic, Language and Information
+%V 13
+%N 3
+%P 287-340
+%D Jun 2004
+
+%A Darren Bane
+%T Computer Algebra Systems, (working paper)
+%I University of Limerick
+%C Ireland
+%D 2004
+%K ban04
+
+%Q Toolsack Software, Ltd.
+%T C++ Coding Standards web page
+%D 2001
+%K too01
+
+%A Todd Hoff
+%T C++ Coding Standard web page
+%D 2002
+%K hof02
+
+%Q Apple Computer, Inc.
+%T Coding Guidelines
+%D 2004
+%K app04
+
+%Q Sun Microsystems, Inc.
+%T Code Conventions for the Java Programming Language
+%D 1999
+%K sun99
+
+%A David L. Parnas
+%T A Procedure of Interface Design, (slides)
+%I University of Limerick
+%C Ireland
+%D 2003
+%K par03
+
+%A Paul C. Clements
+%A R. A. Parker
+%A David L. Parnas
+%A John Shore
+%A Kathryn Britton
+%T A Standard Organization for Specifying Abstract Interfaces
+%R Tech. Rep. 8815
+%I Naval Res. Lab.
+%C Washington, DC, USA
+%D 1984
+%K cle
+
+%A Shimata Tshinanga
+%T Function Applicability System: The Summary, (working paper)
+%I University of Limerick
+%C Ireland
+%D 2004
+%K tsh04
+
+%A Ying Jin
+%A Darren Bane
+%T Application Programming Interfaces Specification of the Kernel, (working paper)
+%I University of Limerick
+%C Ireland
+%D 2004
+%K jb04
+
+%A Eric W. Weisstein
+%T Variable
+%B MathWorld-A Wolfram Web Resource
+%I Wolfram Research, Inc.
+%D 12 Nov 2002
+%K wei
+
+%A Eric W. Weisstein
+%T Rigorous
+%B MathWorld-A Wolfram Web Resource
+%I Wolfram Research, Inc.
+%D 10 Oct 2000
+%K rigorous
+
+%A Brian J. Bauer
+%T Documenting Complicated Programs
+%R Tech. Rep. CRL 316
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 1995
+%K bau95
+
+%A David L. Parnas
+%A Jan Madey
+%T Functional Documents for Computer Systems Engineering
+%J Science of Computer Programming
+%I Elsevier
+%V 25
+%N 1
+%D Oct 1995
+%P 41-61
+%K fundoc
+
+%A Darren Bane
+%T TTS Kernel Module Interface Specs
+%I University of Limerick
+%C Ireland
+%D 2004
+%K ban04
+
+%A Darren Bane
+%T TTS Kernel Expression Language, Version 1.0B
+%I University of Limerick
+%C Ireland
+%D 2004
+%K ban04
+
+%A Brian W. Kernighan
+%A Dennis M. Ritchie
+%T The C Programming language, 2nd ed.
+%I Prentice-Hall
+%C NJ, USA
+%D 1988
+%K kr88
+
+%A Andrew Hunt
+%A David Thomas
+%T The Pragmatic Programmer
+%I Addison Wesley Longman
+%C MA, USA
+%D 2000
+%K ht00
+
+%A Bjarne Stroustrup
+%T The C++ Programming Language, 3rd ed.
+%I Addison Wesley
+%C MA, USA
+%D 1997
+%K str97
+
+%A Hugh Darwen
+%A Christopher J. Date
+%T Towards an Agreeable Model of Type Inheritance
+%K dd
+
+%A Kenneth Baclawski
+%A Bipin Indurkhya
+%T The Notion of Inheritance in Object-Oriented Programming
+%J Communications of the ACM
+%V 37
+%N 9
+%P 118-119
+%D 1994
+%K bi94
+
+%A Andrei Alexandrescu
+%A Petru Marginean
+%T Simplify Your Exception-Safe Code
+%J C/C++ Users Journal, C++ Experts Forum
+%D Dec 2000
+%K am00
+
+%A John Elder
+%T Compiler Construction: A Recursive Descent Model
+%I Prentice Hall International
+%C Hertfordshire, UK
+%D 1994
+%K eld94
+
+%A Shimata Tshinanga
+%T Function Applicability System: Our Proposition of Solution to All Your Concerns, (working paper)
+%I University of Limerick
+%C Ireland
+%D 25 Nov 2004
+%K tsh04
+
+%A Darren Bane
+%T TTS Kernel Standard Library, Version 1.0A
+%I University of Limerick
+%C Ireland
+%D 2005
+%K ban05
+
+%Q ECMA
+%T ECMAScript Language Specification, 3rd ed.
+%I ECMA
+%C Geneva, Switzerland
+%D 1999
+%K ecma99
+
+%Q IEEE/The Open Group
+%T Single UNIX Specification, Version 3
+%I IEEE/The Open Group
+%D 2004
+%K ieee04
+%O Also published as IEEE Standard 1003.1-2004 (POSIX)
+
+%A David L. Parnas
+%A Marius Dragomiroiu
+%T Module Interface Documentation-Using the Trace Function Method (TFM)
+%R Tech. Rep.
+%I University of Limerick
+%C Ireland
+%D 2007
+%K tfm
+
+%A John K. Ousterhout
+%T An Introduction to Tcl and Tk
+%I Addison-Wesley
+%D 1993
+%K ous93
+
+%Q SQRL
+%T Conclusion on the Requirements of the Tools Team
+%D 2004
+%K sqrl04
+
+%A David Abrahams
+%A Nathan Myers
+%T C++ Coding Guidelines
+%D 2001
+%K am01
+
+%A Rob Pike
+%T Notes on Programming in C
+%D 21 Feb 1989
+
+%A Andrei Alexandrescu
+%A John Torjo
+%T Enhancing Assertions
+%J C/C++ Users Journal, C++ Experts Forum
+%D Aug 2003
+%K at03
+
+%A Scott Meyers
+%T More Effective C++
+%I Addison-Wesley
+%D 1996
+%K mey96
+
+%A Ben Shneiderman
+%T Designing the User Interface, 3rd ed.
+%I Addison-Wesley
+%C USA
+%D 1998
+%K shn98
+
+%A Richard Kelsey
+%A William Clinger
+%A Jonathan Rees, (eds)
+%T Revised5 Report on the Algorithmic Language Scheme
+%J Higher Order and Symbolic Computation
+%V 11
+%N 1
+%P 7-105
+%O Reprinted in \fIACM SIGPLAN Notices\fP, 33(9)
+%D 1998
+%K r5rs
+
+%A Maurice Herlihy
+%T Wait-Free Synchronization
+%J ACM Transactions on Programming Languages and Systems
+%V 11
+%N 1
+%P 124-149
+%D 1991
+%K her91
+
+%A Donald E. Knuth
+%T Fundamental Algorithms, 2nd ed.
+%I Addison-Wesley
+%C USA
+%D 1978
+%K knu78
+
+%A Maged M. Michael
+%T Hazard Pointers: Safe Memory Reclamation for Lock-Free Objects
+%J IEEE Transactions on Parallel and Distributed Systems
+%V 15
+%N 6
+%P 491-504
+%D 2004
+%K mic04
+
+%A Nir Shavit
+%A Dan Touitou
+%T Software Transactional Memory
+%B Proceedings of the 14th ACM Symposium on the Principles of Distributed Computing
+%C Ottowa, Ontario, Canada
+%D 1995
+%K st95
+
+%Q Programming Research Group
+%T High-Integrity C++ Coding Standard Manual, Version 2.2
+%D 2004
+%K prg04
+
+%Q Object Management Group
+%T C++ Language Mapping Specification, Version 1.1
+%D 2003
+%K omg03
+
+%A Darren Bane
+%T TTS Kernel Software Requirements, (working paper)
+%I University of Limerick
+%C Ireland
+%D 2005
+%K ban05
+
+%A Darren Bane
+%T TTS Kernel Module Guide, (working paper)
+%I University of Limerick
+%C Ireland
+%D 2005
+%K ban05
+
+%A David L. Parnas
+%T SQRL TTS UE Behaviour Policy, (working paper)
+%I University of Limerick
+%C Ireland
+%D 24 Apr 2006
+%K par06b
+
+%A David L. Parnas
+%T Role of the Kernel in TTS, (working paper)
+%I University of Limerick
+%C Ireland
+%D 28 Sep 2005
+%K par05
+
+%A David L. Parnas
+%A Wolfram Bartussek
+%T Using Assertions About Traces to Write Abstract Specifications for Software Modules
+%R Tech. Rep. TR77-012
+%I University of North Carolina
+%C Chapel Hill, NC, USA
+%O Reprinted in \fISoftware Fundamentals: Collected Papers by David L. Parnas\fP, D. M. Hoffman, D. M. Weiss, eds., Addison-Wesley
+%D 1977
+%K tam
+
+%A Joe Armstrong
+%T Making reliable distributed systems in the presence of software errors
+%I The Royal Institute of Technology
+%C Stockholm, Sweden
+%D Dec 2003
+%K arm03
+
+%A David L. Parnas
+%T On the Criteria to Be Used in Decomposing Systems into Modules
+%J Communications of the ACM
+%V 15
+%N 12
+%P 1053-1058
+%O Reprinted in \fISoftware Fundamentals: Collected Papers by David L. Parnas\fP, D. M. Hoffman, D. M. Weiss, eds., Addison-Wesley
+%D Dec 1972
+%K par72
+
+%A Erich Gamma
+%A Richard Helm
+%A Ralph Johnson
+%A John Vlissides
+%T Design Patterns: Elements of Reusable Object-Oriented Software
+%I Addison-Wesley
+%D 1995
+%K gof
+
+%A Nicolas Dulac
+%A Thomas Viguier
+%A Nancy Leveson
+%A Margaret-Anne Storey
+%T On the Use of Visualization in Formal Requirements Specification
+%B Proceedings of the Conference on Requirements Engineering
+%C Essen, Germany
+%D Sep 2002
+%K vis
+
+%A R. Davis
+%T Runnable Specifications as Design Tool
+%B Logic Programming
+%E K. Clark
+%E S. Tarnlund
+%P 141-149
+%I Academic Press
+%D 1982
+
+%A D. Sannella
+%T Formal program development in Extended ML for the working programmer
+%B Proceedings of the 3rd BCS/FACS Workshop on Refinement, 1990
+%C Hursley Park, UK
+%S Springer Workshops in Computing
+%P 99-130
+%D 1991
+
+%A Gary T. Leavens
+%T An Overview of Larch/C++: Behavioral Specifications for C++ Modules
+%E Haim Kilov
+%E William Harvey
+%B Specification of Behavioral Semantics in Object-Oriented Information Modelling
+%I Kluwer Academic Publishers
+%P 121-142
+%O Chapter 8
+%D 1996
+
+%A Patrice Chalin
+%A Joe Kiniry
+%A Gary T. Leavens
+%A Erik Poll
+%T Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2
+%B Proceedings of Formal Methods for Components and Objects (FMCO 2005)
+%C Amsterdam, The Netherlands
+%D 2006
+
+%A John V. Guttag
+%A James J. Horning
+%A S. J. Garland
+%A K. D. Jones
+%A J. M. Wing
+%T Larch: Languages and Tools for Formal Specification
+%S Texts and Monographs in Computer Science series
+%I Springer-Verlag
+%C NY, USA
+%D 1993
+
+%A D. Crocker, (ed)
+%A P. Overell
+%T RFC 4234: Augmented BNF for Syntax Specifications: ABNF
+%I The Internet Society
+%D Oct 2005
+
+%A Jules Deshernais
+%A Ridha Khe\*'dri
+%A Ali Mili
+%T Towards a Uniform Relational Semantics for Tabular Expressions
+%B RelMiCS
+%P 53-57
+%D 1998
+
+%A Wolfram Kahl
+%T Compositional Syntax and Semantics of Tables
+%R Tech. Rep. SQRL 15
+%I McMaster University
+%C Hamilton, Ontario, Canada
+%D 12 Oct 2003
+
+%A Mark Lawford
+%A P. Froebel
+%A G. Moum
+%T Application of Tabular Methods to the Specification and Verification of a Nuclear Reactor Shutdown System
+%J to appear in Formal Methods in System Design
+%D Jun 2004
+
+%A Gerard J. Holzmann
+%T The Model Checker SPIN
+%J IEEE Transactions on Software Engineering
+%V 23
+%N 5
+%D May 1997
+
+%A David Robertson
+%A Jaume Agust\('i
+%T Software Blueprints: Lightweight Uses of Logic in Conceptual Modelling
+%I Addison Wesley Longman
+%D 1999
+
+%A Wayne Babich
+%T Software Configuration Management: Coordination for Team Productivity
+%I Addison-Wesley
+%D 1986
+
+%A Edsger W. Dijkstra
+%T EWD623: The mathematics behind the Banker's Algorithm
+%D 1977
+%O Reprinted in \fISelected Writings on Computing: A Personal Perspective\fP, Springer-Verlag
+
+%A Edsger W. Dijkstra
+%T EWD123: Cooperating sequential processes
+%D 1968
+%O Published in \fIProgramming Languages: NATO Advanced Study Institute\fP, F. Genuys, ed., Academic Press
+
+%A Colm Quinn
+%A Sergiy A. Vilkomir
+%A David L. Parnas
+%A Srdjan Kostic
+%T Specification of Software Component Requirements Using the Trace Function Method
+%B Proceedings of the International Conference on Software Engineering Advances (ICSEA 2006)
+%D 2006
+
+%A Robert L. Baber
+%A David L. Parnas
+%A Sergiy A. Vilkomir
+%A Paul Harrison
+%A Tony O'Connor
+%T Disciplined Methods of Software Specification: a Case Study
+%B Proceedings of the International Conference on Information Technology Coding and Computing (ITCC 2005)
+%D 2005
+%P 428-437
+
+%A Dale Dougherty
+%A Tim O'Reilly
+%T UNIX text processing
+%I Hayden Books
+%D 1987
+
+%A Colm Quinn
+%T Quality Assessment in Real-time Software
+%I University of Limerick
+%C Ireland
+%D 12 Jun 2007
+
+%A Jacques Carette
+%T Understanding Expression Simplification
+%B Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC 2004)
+%C Santander, Spain
+%D 2004
+
+%A Antoni Diller
+%T Z: An Introduction to Formal Methods, 2nd ed.
+%I Wiley
+%D 1994
+
+%A Chris George
+%T Introduction to RAISE
+%R Tech. Rep. 249
+%I UNU-IIST
+%C Macau, PRC
+%D Apr 2002
+
+%A Gottlob Frege
+%T Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens
+%C Halle, Saxony-Anhalt, Germany
+%I Louis Nebert
+%O Translated by S. Bauer-Mengelberg
+%D 1879
+
+%A Darren Bane
+%T Design and Documentation of the Kernel of a Set of Tools for Working With Tabular Mathematical Expressions
+%I University of Limerick
+%C Ireland
+%D 19 Jul 2008
+%K bane2008
+
+%A Peter Dinges
+%A Naoki YONEZAKI
+%T Structured Operational Semantics for an Idealised Object-Capability Programming Language
+%B Proceedings of the 25th Convention of the Japan Society for Software Science and Technology
+%C Tokyo, Japan
+%D 2008
+
+%A Shin-Cheng Mu
+%A Hsiang-Shang Ko
+%A Patrik Jansson
+%T Algebra of Programming using Dependent Types
+%B Mathematics of Program Construction 2008
+%V 5133
+%S Lecture Notes in Computer Science (LNCS)
+%I Springer-Verlag
+%P 268-283
+%D Jul 2008
+%K muko2008
+
+%A Adrian Mettler
+%A David Wagner
+%A Tyler Close
+%T Joe-E: A Security-Oriented Subset of Java
+%B Proceedings of the 17th Annual Network and Distributed System Security Symposium (ISOC NDSS 2010)
+%C San Diego, California
+%D Mar 2010
+
+%A Chiyan Chen
+%A Hongwei Xi
+%T Combining Programming with Theorem Proving
+%B Proceedings of the 10th International Conference on Functional Programming (ICFP'05)
+%C Tallinn, Estonia
+%D Sep 2005
+
+%A Oleg Kiselyov
+%A Chung-chieh Shan
+%T Lightweight static capabilities
+%J Electronic Notes in Theoretical Computer Science
+%V 174
+%N 7
+%P 79-104
+%D 2007
+
+%A Jonathan S. Shapiro
+%A Michael Scott Doerrie
+%A Eric Northup
+%A Swaroop Sridhar
+%A Mark Miller
+%T Towards a Verified, General-Purpose Operating System Kernel
+%B NICTA Invitational Workshop on Operating System Verification
+%I University of New South Wales
+%C Sydney, Australia
+%D Oct 2004
+
+%A Jessica Gronski
+%A Kenneth Knowles
+%A Aaron Tomb
+%A Stephen N. Freund
+%A Cormac Flanagan
+%T Sage: Hybrid checking for flexible specifications
+%B In Scheme and Functional Programming Workshop
+%D 2006
+%P 93-104
+
+%A Adam Chlipala
+%T Certified Programming with Dependent Types
+%D 3 Feb 2010
+%O available: http://adam.chlipala.net/cpdt/html/toc.html [accessed 18 Aug 2010]
+
+%A Kent Beck
+%T Extreme Programming Explained
+%D 1999
+
+%A Kent Pitman
+%T Accelerating Hindsight: Lisp as a Vehicle for Rapid Prototyping
+%D 1994