diff options
author | Darren Bane <dbane@tilde.institute> | 2020-05-20 23:10:28 +0100 |
---|---|---|
committer | Darren Bane <dbane@tilde.institute> | 2020-05-20 23:10:28 +0100 |
commit | 01c8c655f67f820bc8028d369c5061c997921e72 (patch) | |
tree | 2b42b5838aa05ecbf2223abec31ba6a4d977dd70 /doc | |
parent | 020601c63c8878f82a06d597ae80de94295ef73d (diff) | |
download | lsp-01c8c655f67f820bc8028d369c5061c997921e72.tar.gz |
Blog post generator
Diffstat (limited to 'doc')
-rw-r--r-- | doc/Makefile | 19 | ||||
-rw-r--r-- | doc/breaking_rules.md | 136 | ||||
-rw-r--r-- | doc/refs | 1015 |
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 |