[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> bib
|| [News] || [Research]

Bibliography Retrieval Engine(Beta)

Items in bibliography identified by a string matching LOGIC

AbadiLamport90
.Open AbadiLamport90
 Martin Abadi & Leslie Lamport
 Composing Specifications
 Digital Sys Res Center(Oct 10 1990) CR9405-0309 F.3.1 
.See [AbadiLamport93]
 =MATHEMATICAL SPECIFICATION LOGIC
 Has a ref to Cliff Jones's Oxford PhD Thesis in the early 80s! p9: "Composition is conjunction" cf Zave & Jackson.
.Close

AbadiLamport92
.Open AbadiLamport92
 Martin Abadi & Leslie Lamport
 An Old-fashioned Recipe for Real Time
 Digital Sys Res Center TR#91(Oct 12 1992) 
.See [AbadiLamport94]
 =MATHEMATICAL TIMING LOGIC
.Close

AbadiLamport93
.Open AbadiLamport93
 Martin Abadi & Leslie Lamport
 Composing Specifications
 ACM TOPLAS V15n1(Jan 1993)pp73-132
 =MATHEMATICAL SPECIFICATION LOGIC
 Reviewed CR9405-0309 F.3.1
 similar to AbadiLamport90 Based on Lamport91
.Close

AbadiLamport94
.Open AbadiLamport94
 Martin Abadi & Leslie Lamport
 An Old-fashioned recipe for Real Time
 ACM TOPLAS V16n5(Sep 1994)pp1543-1571 See 
.See [AbadiLamport92]
 =MATHEMATICAL TIMING LOGIC
 Review CR9507-0506 F.3.1: uses TLA as a base
 can reason separately about function and timing(by var now:real). Two problems: now can get stuck (Zeno-ness) or two requirements can conflict. ->> detect and correct spec to avoid. (not in A&L 1992?)
.Close

AbadiLamport95
.Open AbadiLamport95
 Martin Abadi & Leslie Lamport
 Conjoining Specifications
 ACM Ttrans Prog Lang Sys V17n3(May 1995)pp507-535 CR9605-0369 CR9608-0610(...cumbersome notation....) F.3.1
 =MATHEMATICAL SPECIFICATION LOGIC TLA
 conjunction implies parallel combination
.Close

Abiteboul00
.Open Abiteboul00
 Serge Abiteboul & Peter Buneman & Dan Suciu
 Data on the Web: from relations to semistructured data and XML
 Morgan Kaufman SF CA 2000 ISBN 1-55860-622-X CR 0105-0161 QA76.9.D3 A258
 =MONOGRAPH DATA NET/WWW LOGIC XML XSL-QL DTD ACeDB OEM Lore Strudel
.Close

AbramsonDahl89
.Open AbramsonDahl89
 Harvey Abramson & Veronica Dahl
 Logic Grammars
 Springer Verlag 1989
 =HOWTO GRAMMAR DDD PROLOG REALITY
.Close

Abrial89
.Open Abrial89
 J Abrial
 A Formal Approach to Large Software Construction
 In Mathematics of Program construction  J L A Van de Snepscheut(ed) Springer NY NY 1989 pp 1-20. See 
.See [LafontaneLedruSchobbens91]
 =ADVERT LOGIC TOOL Z VDM B
 B theorem prover LOGIC TOOL used by Z and VDM groups
.Close

AgarwalLago95
.Open AgarwalLago95
 Rakesh Agarwal &Patricia Lago
 PATHOS - A Paradigmatic Approach To High-level Object-oriented Software Development
 ACM SIGSOFT Software Engineering Notes V20n2(Apr 1995)pp36-41
 =ADVERT METHOD OBJECT-ORIENTED
.Box
 confused
 technical activities: find classes, find methods and behavior, define classes and methods
 Technical control activities: logical design, detailed design
 ...Early consideration of reuse and quality in design
.Close.Box
.Close

AielloEtAl07
.Open AielloEtAl07
 Marco Aiello & Ian E Pratt-Hartman & Johan F van Bentham (Eds)
 Handbook of spatial Logics
 Springer Verlag NY Secaucus NJ 207 ISBN 1402055862 $CR 0811-1045
 =UNREAD =REFERENCE FORMAL MODAL LOGIC SPACE
.Close

AikenMuntzRichards94
.Open AikenMuntzRichards94
 Peter Aiken & Alice Muntz & Russ Richards
 DoD Legacy Systems: Reverse Engineering Data Requirements
 Comm ACM V37n5(May 1994)pp26-41
 =EXPERIENCE REVERSE ENGINEERING DATA
.Box
1.4 billion LOCs at 1.7K locations in thousands of different systems.

1986..87: Logical Data base Design

1992: First technologically independent logical data model
     LDM has 468 entities and 1994 data elements

1993: LDM has 362 entities and 1318 data elements
.Close.Box
.Close

AlagarVenkatesan01
.Open AlagarVenkatesan01
 Sridhar Alagar & Subbarayan Venkatesan
 Techniques to Tackle state explosion in a Global Predicate Detection
 IEEE Trans Software Engineering  V27n8(Aug 2001)pp704-714
 =THEORY LOGIC MODEL CHECKING
.Close

AlencarCowanLucena02
.Open AlencarCowanLucena02
 Paulo S C Alencar & Donald D Cowan & Carlos J P Lucena
 A Logical Theory of Interfaces and Objects
 IEEE Trans Software Engineering  V28n6(Jun  2002)pp548-575
 =THEORY FORMAL LOGIC CATEGORY OBJECTS INTERFACES ADV ADO
 ADV ::= "Abstract Design Views", interfaces.
 ADO ::= "Abstract Design Objects".
 views_a::@(ADV, ADO).
 cf
.See [AlencarCowanLucenaNova95]
.Close

AlexanderCoplien99
.Open AlexanderCoplien99
 Christopher Alexander & James O Coplien(introduction)
 The Origins of Pattern Theory
 IEEE Software Magazine V16n5(Sep/Oct 1999)pp71-82
 =SPEECH  OOPSLA'96 PATTERN THEORY
 patterns were generative( ala Chomski ), included a moral component, must lead to  morphological coherence - a life promoting structure, a good environment
 15 geometric properties underlying original patterns -> profundity
 80..90%agreement  for "Do you feel more whole/alive in the presence of this or that object?". Correlates with certain features/structures & profound functionallity!
 centers:=field-like structures recursively underlying all wholeness& more or less living things. See 
.See [Alexander00]
 Can/will software designers help people generate a life enhancing world?
.Close

AmblerS97a
.Open AmblerS97a
 Scott Ambler
 Normalizing Classes
 Software Development V5n4(Apr 1997)pp69-72
 =DEMO DATA OBJECT-ORIENTED
 increasing cohesion and coupling by redesign but result is not in even 1NF in Codd terms.
 Adds a repeating group of enrollments to seminar.
 Better: Seminar<-<Enrollment>->Student and `new Enrollment(seminar student)` handles enrollments responsibillities for connecting seminars and students.
 Note: ends up with SSADM composite logical design!
.Close

AmbriolaNotkin88
.Open AmbriolaNotkin88
 V ambriola & D Notkin
 Reasoning About Interactive Systems
 IEEE Trans Softw Eng SE-V14n2(Feb 1988)pp272-276
 =THEORY LOGIC PROOF formal non-sequential
.Close

Ananthaswamy11
.Open Ananthaswamy11
 Anil Ananthaswamy
 I, algorithm
  New Scientist V209n2797 (Jan 29 2011)pp28-31
 =ADVERT =HISTORY AI LOGIC NEURAL NETS MARKOV BAYES PROBABILISTIC PROGRAMMING INFERENCE ENGINE LEARNING LANGUAGES BLOG Church 
 BLOG::language="Bayesian logic".
 Demos of models with thousands of variables. 
 General algorithms are inefficient. 
 Applications: test ban treaty, PhysiScore(babies), QMR-DT
 Ref 
.See [Pearl88]
.Close

Anderson99
.Open Anderson99
 Ross J Anderson
 The Formal Verification of a Payment System
 In 
.See [HincheyBowen99]
pp43-52
 =EXPERIENCE LOGIC BAN VERIFYING PROTOCOL BANKING PAYMENT SMARTCARD
 Used BAN_logic with new rule:
 If A believes that A and B share key K and A sees the K encrypts X then A will believe that B used K.
 Colored proof covering several white boards.
 System successful for several years with problems.
 Concludes the it better to have a simple logic with few rules and no tool than a complex (buggy?) logic with a tool.
.Close

Andrews93
.Open Andrews93
 James H Andrews
 Logic Programming: Operational Semantics & Proof Theory
 Cambridge University Press NY NY 1993 ISBN 0-521-43219-7 CR9503-0142
 =THEORY LANGUAGES
.Close

AndrewsP03
.Open AndrewsP03
 Pater B Andrews
 Introduction to Mathematical Logic and Type Theory: to truth through proof
 Kluwer Acad Pub Norwell MA 2002 ISBN 1402007639 CR 0305-0427
 =THEORY LOGIC TYPES LAMBDA PEANO
.Close

AntoniolGueheneuc06
.Open AntoniolGueheneuc06
 Giuliano Antoniol & Yann-Gael Gueheneuc 
 Feature Identification: an epidemiological metaphor
 IEEE Trans Software Engineering  V32n9(Sep 2006)pp625-641  
 =DEMO MAINTENANCE TECHNICALREVERSE ENGINEERING TOOL CODE MODULE ANALYSIS   
 A way to find out, by executing software the parts used to implement a feature. 
.Close

Antoniou99
.Open Antoniou99
 Grigoris Antoniou
 A Tutorial on Default Logics
 ACM ACM Computing Surveys V31n4(Dec 1999) pp337-359 CR0006-0401
 =TUTORIAL FORMAL LOGIC DEFAULT INFERENCE EXCEPTIONS
 default :=`if Prereq : Justifications then Consequent`, `if Prereq then Consequent unless Justifications is known to be  false` where no free variables in parts.
 default schema has free variables - stands for all substitutions.
 normal: `if P : J then J`
 closed world : `if true : not A then not A`
 Not just inferences but also extensions of sets known facts by applying defaults that don't lead to contradictions
.Close

AntoyHanus10
.Open AntoyHanus10
 Sergio Antoy & Michael Hanus
 Functional Logic Programming  
 Commun ACM V53n4(Apr 2010)pp74- 95
.See http://doi.acm.org/10.1145/1721654.1721675
 =ADVERT CURRY LANGUAGE FUNCTIONAL LOGIC PROGRAMMING 
 Combines ideas from functional programming (LISP, ML, Haskell) and Logic Programming (Prolog).
 Given a definition of a function Curry can sometimes invert it, finding argument values to fit given results. 
.Close

Aptetal80
.Open Aptetal80
 Krzysztof R Apt & Francez & De Roever
 A Proof System for Communicating Sequential Processes
 ACM TOPLAS V2n3(Jul 1980)pp359-385
 =THEORY LOGIC CSP formal
.Close

Asaravala03
.Open Asaravala03
 Amit Asaravala 
 All by themselves
 Software Development Magazine V11n3(Mar  2003)pp38-41
 =HISTORY AGENTS AI Clippy  metadata semantic web XML RDF  ontology DAML+OIL LOGIC
 Agents (minimally) observe an environment and react to changes by interacting with the environment -- and other agents.
 Agents either need a shared ontology or a way to share ontologies and metadata.
 RDF::XML_DTD="Resource Description Framework", indicates relationships between subjects, predicates and objects.
.Close

Astrachan91
.Open Astrachan91
 Owen Astrachan
 Pictures as Invariants
 SIGCSE Bulletin V23n1(Mar 1991)pp112-118
 =DEMO LOGIC TECHNICAL GRAPHIC
.Close

AtleeBuckley96
.Open AtleeBuckley96
 Joanne M Atlee & Michael A Buckley
 A logic-Model Semantics for SCR Software Requirements
 Proc 1996 Int Symposium on Software Testing & Analysis(ISSTA) & ACM SIGSOFT SENotes V21n3(May 1996)pp280-292
 =IDEA LOGIC SCR REQUIREMENTS TABULAR
 SCR::="Software Cost Reduction"
 SCR Statecharts RSML all share conditioned-event-driven reactive systems. demos analytical requirements temporal logic model and tool SMV::="Symbolic Model Verifier". CTL::=Computational Tree Logic
 See CORE
.See [WilliamsL94]
.See [HeimdahlLeveson96]
.Close

Bach95
.Open Bach95
 James Bach
 Enough about process: What we need are heroes
 IEEE Software Magazine V12n2(Mar 1995)pp96-98+replies IEEE Software Magazine V12n3(May 1995)p5-7
.See [Bach9?]
.Box
"Heroism means going beyond the borders of the known world and returning with new knowledge or wealth[...]sustainable, healthy sort of heroism requires judgement to know how much commitmment and risk is right for the situation. The movement towards process in our industry is an understandable reaction against pathological heroism: heroism for its own sake, in which overcommitment and uncontrolled risk-taking is the norm."

p97: "The 'cowboy' or 'big magic' model. In this view, gifted people create software through apparent magical means, with no particular guidance or support"

Can integrate process and heroism by taking a people centred view and seeing software production as a dynamic, complex, etc. system for solving problems.

Reply: John Henry or Pecos Bill, trial by cold pizza,...

.Close.Box
.Close

BaclawskiIndurkhya94
.Open BaclawskiIndurkhya94
 Kenneth Baclawski & Bipin Indurkhya
 The Notion of Inheritance in object-oriented programming(Letter)
 Commun ACM V37n9(Sep 1994)pp118-119
 
.See [Grosberg93]
.See [ArnoldK94]
(C++ advice)
.Box
refers to debate over meaning of inheritance:
 Abrahams's 91 letter "Subject: Objectivism"
 Lalonde & Pugh JOOP 91 "subclassing <> subtyping <> is-a"
 Tesler's 91 CACM letter
  Wegner 80 pages in 90 OOPS messenger
  Winkler 92 letter
refers to POV vs COV in Winkler's letter
Quotes Wegner 90
 POV = Physical & COV = Conceptual
Piaget: Child constructs idea of object permanence from its own actions on the objects.

Class of objects without actions<>class of objects with some actions.

Failure to find epistomological foundations of the IS-A link - six different generic-generic and four kinds of generic-individual relation

"The point here is that the concepts in the real world, which programs attempt to model, do not come in neatly packaged hierarchies." (cf GoldsteinAlger92)

"There are no standard conceptual hierachies. Given a domain and a specific
PURPOSE, certain concept hierarchies would be clearly preferable than 
others, but such policy decisions are best left to the USER of the 
programming language[...] What a PL provides is a set of mechanisms [...] 
restrict what can be implemented[but] they do not themselves validate some
view of inheritance or other[...]" these are also just implemented concepts
and do not not have a universal objective meaning....upto the designers to
choose suitable mechanisms.
.Close.Box
.Close

BaierHaverkortHermansKatoen03
.Open BaierHaverkortHermansKatoen03
 Christel Baier & Boudewijn Haverkort & Holger Hermans & Joost-Pieter Katoen
 Model-checking algorithms for continuous-time Markov Chains
 IEEE Trans Software Engineering  V29n6(Jun 2003)pp524-541
 =THEORY MATHEMATICS MODEL CHECKING CTMC CSL RELIABILITY  CTL
 CSL:="Continuous Stochastic Logic". Steady state + path probabilities in time intervals. Modes P[event] <=> p. Nested. Generalizes CTL.
 CTMC::="continuous time Markov chains". P(i -> j fires after t) = c*exp( -rate*t) iff it is first.
 
.Close

BaierEtAl07
.Open BaierEtAl07
 Christel Baier & Lucia Cloth & Boudewijn R Haverkort & Mathias Kuntz & Markus Siegle 
 Model Checking Markov Chains with Actions and State Labels
 IEEE Trans Software Engineering  V33n4(Apr 2007)pp209-224 
 =THEORY MODEL CHECKING REAL TIME MARKOV CHAINS PROBABILITY LOGIC asCSL
 Logic + model design for verifying requirements that a given pattern of actions and states (and time limits) has a given range of probabilities.  
 Example requirement: the probabillity of entering a `full` state via a number of `arrive` actions within 5 time units must be greater than or equal to 99%.
 Defines products of chains.
 Cellular phone hand over model.
 experiment with tool.
.Close

BaierKatoen08
.Open BaierKatoen08
 Christel Baier & Joost Katoen
 Principles of Model Checking
 The MIT Press Cambridge MA (2008) ISBN 026202649X $CR 0912-1115
 =TEXT =THEORY MODEL CHECKING MODAL LOGICS FSM LTL CTL CTL* TCTL BISIMULAION OBDT MARKOV PCTL PCTL*
 Excellent and thorough text book suitable for graduate Computer 
scientists or some final year undergraduates
 A large in depth reference to the theory of the most successful 
formal methods - so far.
 Does not use the normal syntax for modes but uses \forall and \exists.
So doesn't fit some tools.
 Does not use standard terminology.
 Does include newer topics and types of models.
.Close

BaierHaverkortHermansKatoen10
.Open BaierHaverkortHermansKatoen10
 Christel Baier & Boudewign R Haverkort & Holger Hermans & Joost-Pieter Katoen
 Performance Evaluation and Model Checking Join Forces
 Commun ACM V53n9(Sep 2010)pp76-85  
.See http://doi.acm.org/10.1145/1810891.1810912
 =HISTORY MODEL CHECKING PERFORMANCE MODAL PROBABILLITY LOGIC CTL LTL PCTL DTMC ADVERT TOOLS PRISM EXAMPLES
 Excellent diagram of history starting with Markov Chains in 1900 and ending with advanced algorithms and applications.
 Figure 3: IPv4 zeroconf protocol
 Example -- able to show that Firewire root contention protocol is faster when biased "coin tossing" is used.
.Close

Ballanceetal90
.Open Ballanceetal90
 Robert A Ballance & Susan L Graham & Michael L Van De Vanter
 The Pan Language-Based Editing System for Integrated Development Environments
 SIGSOFT'90 pp77-93
 p85 Logic programming
.Close

BarbierEtal03
.Open BarbierEtal03
 Franck Barbier & Brian Henderson-Sellers & Annig Le Parc-Lacarelle & Jean-Michele Bruel
 Formalization of the Whole-Part Relationship in the Unified Modeling Language
 IEEE Trans Software Engineering  V29n5(May 2003)pp459-470
Reviewed $CR 0409-1078 and 0409-1079
 =PROPOSAL  Object-Oriented MODEL STANDARD aggregation composition whole-part bibliography UML OCL MetaModel  OML OPEN Diamonds
 careful philosophical analysis of semantics of whole-part.  some confused "common logic" and much OCL.
 Defines a new dotted diamond whole-part  Relationship with specialization of aggregation and composition.
 Introduces new stereotypes to indicate OCL constraints on the UML MetaModel.
 Will it make it into UML4.0?
 Correspondence
.Box
  IEEE Trans Software Engineering V29n11(Nov 2003)pp1054-1056
 "On formalization of the whole-part relationship in the unified modeling Language" by Hee Beng Kuan Tan & Lun Hao & Yong Hang corrects 
discrepancies,
 "Controversies about the Black and White Diamonds" by Frank Barbier & Brian Henderson-Sellers" responds by changing name of "antisymmetry", accepting new formula for "transitivity", and agreeing to minor correction in a proof. Regrets the absence of "scientific" review of UML specifications.

.Close.Box
.Close

Barjis08
.Open Barjis08
 Joseph Barjis
 The importance of business process modeling in software systems design
 Science of Computer Programming V71n1(Mar 2008)pp73-87
.See http://www.sciencedirect.com/science $CR 0906-0558
 =ADVERT METHOD THEORY MODEL DEMO LANGUAGE-ACTION PETRI GRAPHIC ANALYSIS REQUIREMENTS SCENARIOS
Keywords: Requirements specifications; Model checking; Business process modeling; Business process simulation;
 DEMO::="Design & Engineering Methodology for Organizations",
.See http://www.demo.nl/
 Special colored Petri nets show logic. Can be simulated to show clients what is possible.
 Analyze business processes in terms of the language-action cycle as expressed as $Transactions between parts.
 Transaction::=Order; Execution; Result.
 Order is a transition from initiator to executor. It sets up a contract for the executor to carry out.
 Result is a transition from executor to initiator.  It completes the contract.
 Execution is executed by the executor and can initiate further transactions with others.
.Close

Barnhart99
.Open Barnhart99
 Andy Barnhart
 Wrapping COBOL Business Logic in Java
 Software Development Mag V7n10(Oct 1999)pp41-45.
 =EXPERIENCE TECHNICAL COBOL JAVA GUI LEGACY
 MARS UK RLSCOM Telco marketting cellular air time
.Close

Barrett87
.Open Barrett87
 Geof Barrett
 Formal Methods Applied to a Floating Point Number System
 Technical Monograph 58 PRG Oxford 1987
 =EXPERIENCE PROOF Floating-point operations STANDARD
.Box
used Hoare/Floyd-style proofs to prove that Inmos' software
floating-point package satisfied its specification, a Z-ified version of
the IEEE-754 standard. This software fp package was the starting point for the formally-derived microcode for the FPU in the Inmos T800 transputer. This was certainly a real-world application; moreover, the formal approach overtook the informal approach, and in the process they found an inconsistency and an ambiguity in the IEEE standard, and a bug in a competitor's chip. Inmos and the PRG (Oxford) were awarded a Queen's Award for Technological Achievement for the T800 project.

Includes Floating point IEEE TSE paper -- where is it?
.Close.Box
.Close

BaudryEtal05
.Open BaudryEtal05
 Benoit Baudry  & Franck Fleurey & Jean-Marfc Jezequel & Yves Le Traon
 Automatic Test Case Optimization: A Bacteriologic Algorithm
 IEEE Software Magazine V22n2(Mar/Apr 2005)pp76-81
 =IDEA C# PARSER BUILDER VISITOR TESTING MUTATION EVOLUTION FITNESS
 Nice use of patterns in the sample Component Under Test (CUT) a C# parser.
 Need 30 generations to produce a set of tests that could `kill` all 500 mutants.
.Close

Beck01
.Open Beck01
 Kent Beck
 Aim, Fire
 IEEE Software Magazine V18n5(Sep/Oct 2001)pp87-89
 =DEMO TESTING first is ANALYSIS DESIGN  SPECIFICATION
 "Never write a line of functional code without a broken test case".
 Ward Cunningham: "Test-first coding is not a testing technique".
 Writing tests helps you understand the problem: analysis.
 Writing tests described the logic of the design.
  Hard to write GUI tests.
 Claim that creatively lazy test-first coding tends to be more cohesive and less coupled -- because the interfaces tend to be minimized to saving typing: "intense feedback substitutes for the ability to guess right"
 Test cases expose misunderstandings in pair programming.
 Test cases document the all important answer to "What was this idiot thinking when he wrote this?".
.Close

Beeson81
.Open Beeson81
 Michael J Beeson
 Formalizing Constructive Mathematics: Why and How?
 Constructive Mathematics Spring Verlag Lecture Notes in Mathemetics V873 pp146-190 1981
 =THEORY FORMAL LOGIC
LPT::="Logic of Partial Terms"
 Compare 
.See [Schock68]
.See [Parnas93]
.See [JonesCB95]
and
.See [PVS]
LPF:=Logic of Partial Functions
.Close

BelliniMattoliniNesi00
.Open BelliniMattoliniNesi00
 P Bellini & R Mattolini & P Nesi
 Temporal Logics for Real-time system specification
 ACM Computing Surveys V32n1(Mar 2000) pp12-42
 =SURVEY LOGIC TIMING RTL RTIL RTTL
 WWW link to ACM Digital Library:
.See http://www.acm.org/pubs/citations/journals/surveys/2000-32-1/p12-bellini
 From Abstract: 
 The specification of reactive and real-time systems must be supported by
formal, mathematically-founded methods in order to be satisfactory and
reliable. Temporal logics have been used to this end for several years.
Temporal logics allow the specification of system behavior in terms of
logical formulas, including temporal constraints, events, and the
relationships between the two. In the last ten years, temporal logics have
reached a high degree of expressiveness. Most of the temporal logics
proposed in the last few years can be used for specifying reactive systems,
although not all are suitable for specifying real-time systems. In this
paper we present a series of criteria for assessing the capabilities of
temporal logics for the specification, validation, and verification of
real-time systems. Among the criteria are the logic's expressiveness, the
logic's order, presence of a metric for time, the type of temporal
operators, the fundamental time entity, and the structure of time. We
examine a selection of temporal logics proposed in the literature. To make
the comparison clearer, a set of typical specifications is identified and
used with most of the temporal logics considered, thus presenting the reader
with a number of real examples.
.Close

Ben-Ari10
.Open Ben-Ari10
  Mordechai (Moti) Ben-Ari
  A Primer on Model checking
  ACM Inroads V1n1(Mar 2010)pp40-47
  =ADVERT =EXAMPLES MODEL CHECKING EDUCATION Spin VN Erigone NDFA 
NON_SEQUENTIAL VERIFICATION MODAL LOGIC Promela IDE
  The formula `if not p then if p then q` can be proved true by 
axiomatic methods but it is simpler and easier to check that it is 
true by trying out all 4 cases in a truth table.
  Similarly, proving that a parallele non-deterministic program has a 
property is usually time consuming but there exist tools that will 
find counter examples in a reasonable time.
Spin works in industry but can be wrapped in an IDE that works well 
with students.
.Close

BergmanMoorNelson90
.Open BergmanMoorNelson90
 Merrie Bergman & James Moor & Jack Nelson
 The Logic Book (2nd edn)
 McGrawHill (1990) ISBN 0-07-909524-0 LC# BC135.B435
 =TEXT FORMAL LOGIC NATURAL DEDUCTION TREES SEMANTIC TABLEAUX
.Close

BerryKamsties05
.Open BerryKamsties05
 Daniel M Berry & Erik Kamsties
 The syntactically dangerous ALL and Plural in Specifications
 IEEE Software Magazine V22n1(Jan /Feb 2005)pp55-57
 =IDEA AMBIGUITY LOGIC  LANGUAGE SPECIFICATION CS565
 Words to suspect: "only", "all", "also", "each".
 Use "each" when describing a property of the individual members of a set.
 Use "all" for shared properties across a set.
 Can use simple logic to clarify an ambiguity.
 All the lights in the room have a single on-off switch.
.Net
 Each light has its own switch.
 For all y:lights_in_room, one x: switch (x is on_off_switch_for y).
 All the lights share a common switch.
 For one x: switch,  all y:lights_in_room (x is on_off_switch_for y).
.Close.Net
 Similarly for plurals: "Students enroll in six courses" vs "Students enroll in hundreds of courses".
.Close

BeyerNoackLewerentz05
.Open BeyerNoackLewerentz05
 Dirk Beyer & Andreas Noack & Claus Lewerentz
 Efficient Relational Calculation for Software Analysis
 IEEE Trans Software Engineering  V31n2(Feb 2005)pp137-149
 =TOOL RELATIONAL LOGIC RML BDD TECHNICAL PATTERN JAVA CrocoPat
 Faster recognition of patterns in class structures tested faster on real code: JDK AWT, Eclipse,... Than Prolog and MySQL.
.Close

BiZhao04
.Open BiZhao04
 Henry H Bi & J Zhao 
 Applying propositional logic to workflow verification 
 Information Technology and ManagementV5n3-4(Jul wppr)pp293-318 $CR 0605-0526
  =UNREAD =THEORY WORKFLOW VERIFICATION LOGIC
.Hole
.Close

Blikle77
.Open Blikle77
 Andrzej Blikle
 Co-Routines and Networks of Parallel Processes
 Proc IFIP 77 (North Holland Pub Co 1977) pp285-290. Also IRIA Raport de Recherche No 202 Nov 76
 =THEORY LOGIC SEMANTICS REGULAR-EXPRESSIONS
.Close

Bliss42
.Open Bliss42
 Charles K Bliss
 Semantography ( Blissymbolics) 2nd Edn
 Semantography ( Blissymbolics), Sydney Australia 1942
.See http://www.semantography.com/
 =ADVERT GRAPHIC SYMBOLIC LANGUAGE GENERAL SEMANTICS RATIONALITY LOGIC
 Explains BlissSymbolics.
 Argues that Semantography helps spot crooked thinking and false arguments.
 Bliss Symbols include all internationally agreeed symbols: Math, Chem, Music,...
 Dictionary of symbols
.See http://www.semantography.com/4/
.Close

BloomEsik93
.Open BloomEsik93
 Stephen L Bloom & Zoltan Esik
 Iteration Theories: Equational Logic of Iterative Processes
 EATCS monographs on Theoretical Computer Science Springer Verlag NY NY 1993 ISBN 0-387-56378-4 CR9505-0287 630 pages $109.00 Hardcover
 =MATHEMATICAL LOGIC ALGEBRA SEMANTICS
.Box
Blurb: detailed investigation of the fixpoint/iteration operation. Universal Algebra.
Correctness logic is a special case of the equational logic of Iteration theories.
Ten year program... see Bloom83
CR9505-0287: categegory theory, slow and casual, nonstandard power functor, doesn't discuss dynamic algebras, algebras with star, action algebras, or process algebras.
.Close.Box
.Close

BojicVelasevic00
.Open BojicVelasevic00
 Dragan Bojic & Dusan Velasevic
 Reverse Engineering of Use Case Realizations in U ML
 ACM SIGSOFT Software Engineering notes V25n4(Jul 2000)pp56-61
 =IDEA VisualC++ TEST profiling LOGIC DA-C
 use concept analysis to  convert profiles of test executions into lattices of use-cases
.Close

BoralvStalmarck99
.Open BoralvStalmarck99
 Arne Boralv & Gunnar Stalmarck
 Formal Verification in Railways
 In 
.See [HincheyBowen99]
pp329-350
 =EXPERIENCE RISKS SPECIFICATION STD/FSM LOGIC TPA vs DESIGN V&V TOOL Prover Delphi for ADtranz CVT Swedish Sternol
 Prover is a Company specializing in the industrialization of formal methods. Stalmarck has patented the proof algorithm!
 Can we make a formal tool that is as transparent to use as a word processor?  Some parts need a formal methods expert, but some parts can be made more useful to railway interlocking engineers.
 Need to trade-off expressive power of logic with the performance of the tool.
 Claims that ONLY domain/application knowledge is needed to use the tools.
.Close

BorgerSchulte00
.Open BorgerSchulte00
 Egon Bo"rger & Wolfram Schulte
 A Practical Method for Specification and Analysis of Exception Handling -- A Java/JVM Case Study
 IEEE Trans Software Engineering  V26n9(Sep 2000)pp872-887
 =CASESTUDY LOGIC SPECIFICATION SEMANTICS JAVA COMPILER JVM PROOF
.Close

Borgidaetal95
.Open Borgidaetal95
 Alex Borgida & John Mylopoulos & Raymond Reiter
 The frame problem in procedure specifications
 IEEE Trans on Software Eng VSE-SE-21n10(Oct 1995)pp785-798
 =CRITIQUE LOGIC Set Theory SPECIFICATION METHODS circumscription
.See [BorgidaMylopoulosReiter93]
.Find JacksonD9
.See [McCarthy87]
.See [Delgrande98]
.Close

BorgidaJarke92
.Open BorgidaJarke92
 Alex Borgida & Mathias Jarke
 Knowledge and Representation in Software Engineering(Editorial on special issue)
 IEEE Trans SE-18n6(Jun 1992)pp449-450 CR9307-0467
 domain logic ... relation to formal methods ... power vs performance ... empirical results
.Close

Botting78a
.Open Botting78a
 Richard J Botting
 Loglan -- a more flexible language
 =ADVERT Loglan Mathematics Logic  ITL UNIVERSAL LANGUAGES
 Computer Weekly (UK) n598 (Feb 16 1978)letters
 Response to
.See [Kelly78]
 Argues that Loglan fits Kelly's criteria better.
.Close

Botting86a
.Open Botting86a
 RJ Botting
 Into the Fourth Dimension: An Introduction to Dynamic Analysis & Design
 SE Notes v11 n2 pp36-48 Apr 1986 ACM SIG Software Engineering
 =THEORY DAD graphic logic Reality
.Close

Botting87b
.Open Botting87b
 RJ Botting
 Regular Expressions Relations & Software: Part I - Practice & Part II - Theory
 Western Educational Computing Conference Nov 1987 Western Periodicals Co. N Hollywood CA.
 =THEORY DDD JSP theory languages logic formal
.Close

Boute00
.Open Boute00
 Raymond T Boute
 Supertotal function definition in Mathematics and Software Engineering
 IEEE Trans Software Engineering  V26n7(Jul 2000)pp662-672
 =IDEA FORMAL LOGIC FUNCTIONAL  MATHEMATICS calculational
 Refers to FunMath 
.See [PVS]

.See [Parnas93]
 Compare: 
.See [LPT]
 Question: How to calculated easily with partial functions?
 Idea: Functions defined by a domain and an expression can be treated as total by extension to an arbitrary value in calculating with suitably guarded formulae
.Close

BowdigeGriswold98
.Open BowdigeGriswold98
 Robert W Bowidge & William G Griswold
 Supporting the Restructuring of Data Abstractionns through Manipulation of a Program Visulaization
 ACM TOSEM V7n2(Apr 1998)pp109-157
 =TOOL TECHNICAL GRAPHIC ADT REENGINEER
.Close
Bowen00
 Jonathon Bowen
 The Ethics of Safety-Critical systems
 Commun ACM V43n4 (Apr 2000)91-97
 =ESSAY RISKS METHODS Aristotle LOGIC
 7  sins: epideictic, hyperole, pistic, oligarchy, ephemeral, epexegesis , maiandos
  principles
 modes of thought: scientific, technical, prudence, inntelligence/intuition, wisdom
 p93: "most theorems are correct, but most hand proofs are wrong"
.Close

Bowen01
.Open Bowen01
 Jonathon P Bowen
 Experience Teaching Z with TOOL and Web Support
 ACM SIGSOFT Software Engineering Notes V26n2(Mar 2001)pp69-75
 =REPORT UK TEACHING MATHEMATICAL LOGICAL SPECIFICATION REFINEMENT TOOLS ZTC ZANS
 Diagnostic quizzes leading to makeup tutorials help handle wide ranges of math skills.
.Close

BowenHinchey94
.Open BowenHinchey94
 Jonathan P Bowen & Michael G Hinchey
 Formal Methods andSafety Critical Standards
 IEEE Computer Magazine V27n8(Aug 1994)pp68-71
.Box
Quotes IEEE standard definitions
Most standards are reccommending formal methods rather than mandating them or using them.
Table 1, p70: shows that only 1 out of 5 US standards has FMs, but all 7 non-US standards have FMS

FMs mentioned in standards: CCS(2), CSP(2), HOL(2), LOTOS(2), OBJ(2), Temporal Logic(2), VDM(3), Z(4)
.Close.Box
.Close

BrewkaEiterTruszczynski11
.Open BrewkaEiterTruszczynski11
 Gerard Brewka & Thomas Eiter & Miroslav Truszczynski 
 Answer set programming at a glance
  Commun ACM V54n12(Dec 2011)93-103 
.See http://doi.acm.org/10.1145/2043174.2043195
 =ADVERT DEFEASIBLE LOGIC DECLARATIVE PROGRAMMING ASP GROUNDERS SATISFY SAT SEMANTICS TOOLS APPLICATIONS ABBREVIATIONS
 a <- b1,...,bm, not c1, ..., not cm.
where a,b,c... are "predicates'.
 Answer set is a set of predicates that can be derived if we assume certain predicates  are true/false and is not contradicted by the derivable predicates.
 Able to express if-then-else and constraints easily and a number of other formulas that appear in practice.
 Can handle predicates that contain variables by reducing them.
.Close

Britcher96
.Open Britcher96
 Bob Britcher
 A Few (proposed) fundamental laws of programming
 IEEE Computer Magazine V29N3(Mar 1996)p136(Open channel)
.Box
The Law of Rapid Specialization
  In programming major changes in the product can occur in an instant
      vs time to change plant or physical products

The Law of Fallibility
   The most careful reasoning about a simple sentence can lead to a wrong conclusion about the real world
     Programmers have to reduce big "word-problems" to logic.

The Law of Intellectual Gravity
   Programs can be as massive(in there own way) as physical objcts.

The Law of Permannence
   Programs do not become extinct.  They are not discarded, they are piled up, combined, absorbed, breeding and spreading.
.Close.Box
.Close

BrockHunt99
.Open BrockHunt99
 Bishop C Brock & Warren A Hunt Jr
 Formal Analysis of the Motorola CAP DSP
 In 
.See [HincheyBowen99]
pp-
 =EXPERIENCE HARDWARE DESIGN V&V VERIFICATION FORMAL LOGIC TOOL ACL2
.Close

BrownP91
.Open BrownP91
 Patrick Brown
 Integrated hypertext and program understanding tools
 IBM Syst J V30n3(1991)pp363-392
 =TOOL TECHNICAL
 CR 9211-0872(N Zvegintov)
.Box
CR92011-0875 is by N Zvegintov and refers to the lack of tools to record and maintain links between the domain and the implementation.

Multiple{languages, platforms(IBM), uses, data/tools}

ISEA Integrated SoftwareEngineering Applications tools platform OS/2 + VM + MVS, Distributed client &/| server

CodeNavigator helps programmers {undertand software,  analying change requests, Diagnosis}
{what, where, how}-used, flows{logic, calling,...}, annotations, source code brousing

p369 "Program analysis can create databases that may grow to many times the size of the original source library"

500KLOC -> too big for wkstn DB

Staged analysis, raw vs derived data

flexible USER interfaces

TRAILS::= prototype hypertext tool

linking program data - HIPO | lexical afinity  |Data model attributes

p389: "Lost in Hyperspace" - "loosing track of what they are looking at or how they got there"

.Close.Box
.Close

Broy11
.Open Broy11
 Manfred Broy
 Can Practitioners neglect theory and theoreticians Neglect practice?
 IEEE Computer V44n10(Oct 2011)pp19-24
 =ESSAY GAP THEORY ENGINEERING
 Theory should help establish terminology, techniques, and measurements.
Practicioners have provided good ideas but where is the scientific tests of these theories?
 Craft, Science, or Engineering?
 Theory should help organize knowledge -- both domain and technical knowledge
 A method/methodology may not have an explicit theory and probably:
does not scle, is too difficult, not well designed, and not cost-effective.
 Theory should be part of a software enginmeers education: operating systems, data bases, protocols, formal languages, semantics,...
.Key informatics,
sociology,...
 Theory in research: based on empirical data, isolated, vs ad hoc methods.
 We do not need beautiful theories -- we need to solve particular problems.
 Other forms of engineering a based on separate sciences... software engineering
depends on logics and theories of  information and computation.
.Close

Buchi02
.Open Buchi02
 J R Buchi
 On a Decision Method in Restricted second-order arithmetics
 Proc Int'l Conf. Logic, Methods and philosophy of science (1962) pp1-12
 =THEORY AUTOMATA omega-automata Buchi-automata 
 Given a standard finite state automata with accepting states its language
is defines a set of infinite strings that are acceptable: they can return 
an infinite number of times to at least on of the accepting states.
.Close

Burge91
.Open Burge91
 T Burge
 Truth and Singular Terms
 in Philosophical Applications of Free Logic Oxford Univ Press 1991 pp 189-204
 =THEORY FORMAL LOGIC
 See 
.See [LPT]
 and 
.See [LPV]
.Close

BurrowsAbadiNeedham89
.Open BurrowsAbadiNeedham89
 M Burrows & M Abadi & R M Needham
 A Logic of  Authentication
 Proc Royal Society of London A V426(1989)pp233-271
 =THEORY FORMAL LOGIC
  BAN_logic::Logic,  logic of authentication -- who can believe what about whom?
.See http://csci.csusb.edu/dick/samples/BAN.html
 See also 
.See [BurrowsAbadiNeedham90]
.Close

BurrowsAbadiNeedham90
.Open BurrowsAbadiNeedham90
 Michael Burrows & Martin Abadi & Roger M Needham
 A Logic of Authentication
 ACM Transactions on Computer Systems V8n1(Feb 1990)pp18-36
.See http://doi.acm.org/10.1145/77648.77649
 =THEORY =DEMO LOGIC PROTOCOL PROOF V&V BAN KERBEROS CRYPTO
 See also 
.See [BurrowsAbadiNeedham89]
 Defines the 
.See [BAN_logic]
of beliefs and messages.
.Close

CalcagnoOHearnBornat03
.Open CalcagnoOHearnBornat03
 C Calcagno & P OHearn & R Bornat
 Program logic and equivalence in the presence of garbage collection
 Theoretical Computer Science V298n3(??? 2003)pp557-581
 =THEORY FORMAL LOGIC HOARE  Garbage Collection (D.4.2) VERIFICATION
 What do we mean when we say that a particular object "exists" on the heap?  To preserve Hoare's assignment axiom in the presence of garbage collection, the existence of garbage becomes "virtual".
 The wise program prover should use a language with proved automatic garbage collection, and avoid assertions that refer to garbage!
 Includes a formal model of garbage collection.
.Close

CalinescoGhezziKwiatowskaMirandola12
.Open CalinescoGhezziKwiatowskaMirandola12
  Radu Calinescu & Carlo Ghezzi & Marta Kwiatowska & Raffaela Mirandola
  Self-adaptive Software needs Quantitative Verification at runtime
  Commun ACM V55n9(Sep 2012)pp69-77
.See http://doi.acm.org/10.1145/2330667.2330686
  =THEORY ADAPTIVE PERFORMANCE MONITOR ADJUST DTMC PCTL SERVICE 
 Need to verify:  `If Specification and Domain then Requirement`.
 Non-standard activity diagrams look good...
 Markovian model of the specification, Probalistic Computer Treel Logic requirements.
 Domain data comes from monitoring service performance.
 System can switch components if performance is bad.
.Close

Camilleri90
.Open Camilleri90
 Albert John Camilleri
 Mechanizing CSP Trace Theory in Higher Order Logic
 IEEE Trans Software Engineering SE-V16n9(Sep 1990)
.Close

Campbell-Kelly10b
.Open Campbell-Kelly10b
 Martin Campbell-Kelly
 Historical Reflections: Victorian Data Processing
 Commun ACM V53n10(Oct 2010)pp19-21 
.See http://doi.acm.org/10.1145/1831407.1831417
 =HISTORY DATA PROCESSING LOGICAL vs PHYSICAL BABBAGE CLEARING CHECKS USA CHEQUES  UK 
 Shows an efficient solution to a problem in the form of a multi-agent procedure.
 Traces the evolution of Bank Clearing Houses in the UK (as documented by Babbage) and then in the USA.
 Argues that similar algorithms are still used in modern information technology.
.Close

Canforaetal92
.Open Canforaetal92
 Gerardo Canfora & Anielo Cimitile & Ugo de Carlini
 A Logic-Based Approach to Reverse Engineering Tools Production
 IEEE Trans on Software Eng VSE-18n12(Dec 1992)pp1053-1064
.Box
Prolog model of a Pascal-like program gives queriable data base/knowledge base.

Implemented on silicon/UNSW Prolog.
.Close.Box
.Close

CaplanHarandi95
.Open CaplanHarandi95
 Joshua E Caplan & Mehdi T Harandi(*@cs.uiuc.edu)
 A Logical Framework for Software Proof Reuse
.See [SamadzadehZand95] pp106-113
 =THEORY DEMO PROOF REUSE
 Hoare triples do not have referential transparency!
.Box
Created a new quantifier to bind (and hide) program identifiers into a context and protect them from sustitution.  deca;arations also bind identifiers (and so hide them).

Assignment axiom:
  for_vars x( {P(t=>x[m])} x[m]:= t {P} ).
Declaration axiom:
  for_vars x({ P and x[m]=e} C{Q})
  ---------------------------------------------------where x=y,x[m],z.
  for_vars y,z( {P} new x[m]:=e ; C {Q} )
.Close.Box
.Close

Carroll94
.Open Carroll94
 John M Carroll<carroll@cs.vt.edu>
 Making Use a Design Representation
 Commun ACM V37n12(Dec 1994)pp29-35
 =EXPERIENCE USER scenario use-case
.Box
Scenarios have always been an informal but useful part of documentation.  Make them the prime representation of the system instead -- reason with them....

Also include analysis of psychological effects of technical decision: IN <situation> <a feature> CAUSES < + effect> BUT MAY ALSO CAUSE < - effect>
.Close.Box
.Close

CarrollL77
.Open CarrollL77
 Lewis Carroll (ed. William W Bartley III)
 Symbolic Logic Pts I & II
 Harvester Press 1977 Hassocks Sussex England
 =MONOGRAPH LOGIC syllogisms SORITES EXAMPLES
 Pt II uses something like resolution and semantic tableaux!
.Close

CerroGasquet02
.Open CerroGasquet02
 Luis Farnias Del Cerro & Olivier Gasquet
 A General Framework for Pattern-Driven Modal Tableaux
 L J of the IGPL V10n1(2002)pp51-83
 =THEORY PROVING MODAL LOGIC SEMANTIC TABLEAUX RELATIONS
 Proves completeness and soundness for a set of rules for proving formula in many different modal logics by combining Kripke semantics, semantic Tableaux, and relational calculus.
 p58 rule <>: If <>A,S @ p then add node q: <>A,S@p ---A@q.
 rule K: if []A,S@p----S1@q then  []A,S@p----A,S1@q.
 Lotrec::tool=http://www.itit.fr/ACTIVITIES/LILaC/Lotrec/,
written in Java
.Close

Cervanto00
.Open Cervanto00
 Iliano Cervanto
 Logical Framework: Why not  just classical logic?
 CSLI Lecture notes V91, Stanford U(2000)pp87-104
in "Formalizing the dynamics of information" ed. Martina Faller & Stefan C Kaufmann & Marc Pauly ISBN 1-57586-239-5 Q360
 =ESSAY LOGIC LAMBDA cf Z SCHEMA
 (dick)  |-  Parallels my thinking in creating MATHS.
.Close

Chalin10
.Open Chalin10
 Patrice Chalin
 Engineering a sound assertion semantics for the verifying compiler
 IEEE Trans Software Engineering V36n2(Mar/Apr 2010)pp275-287
 =TYPE USER V&V SQA FORMAL METHOD TOOL VC VERIFICATION COMPILER
  A verifying compiler should spot when assertions will go wrong. 
 The logic of the verifying compiler should allow for expressions being undefined.
 Must handle arithmetic errors like 1/0 correctly. Even in assertions! 
 Stresses the need to talk to the users of the compiler before deciding its semantics!
 Introduces a definedness predicate. 
 Formal Methods shouldn't have imposed an elegant but unsound logic on software.
.Close

Champeaux02
.Open Champeaux02
 Dennis de Champeaux
 Software Engineering Considered Harmful
 Commun ACM V45n11(Nov 2002)pp102-104
 =ESSAY ENGINEERING SCIENCE LOGIC PRACTICE C++UML VALIDATION
 Quotes Denning on the state of current software systems and being hired to fix messes that should not have occurred.
 Need for extensions to Hoare Logic to pointers and parallel processes.
 Seems to ignore work by Hoare, Lamport and others.
.Close

ChanEtal01
.Open ChanEtal01
 William Chan & Richard J Anderson & Paul Beame & David H Jones & David Notkin & William E Warner
 Optimizing symbolic Model checking for Statecharts
 IEEE Trans Software Engineering  V27n2(Feb 2001)pp170-190, also in ICSE'99
 =EXPERIMENTS FORMAL VERIFICATION REQUIREMENTS STATECHARTS GRAPHIC LOGIC OPTIMIZATION RSML TCAS II BDD
 Electrical power distribution system
 order of magnitude improvements.
.Close

ChariSeshadri04
.Open ChariSeshadri04
 Kaushal Chari & Saravanan Seshadri
 Demystifying Integration
 Commun ACM V47n7(Jul 2004)pp59-63
 =TAXONOMY STANDARDS BUSINESS
 (industry domain (independent  | dependent ))><((data  |  business  | presentation ) logic)><(( transport | data format | process  ) level)
.Close

ChechikDevereuxEasterbrookGurfinkel04
.Open ChechikDevereuxEasterbrookGurfinkel04
 Marsha Chechik & Benet Devereux & Steve Easterbrook & Arie Gurfinkel
 Multi-Valued Symbolic Model-Checking
 ACM TOSEM Trans Software Eng & Methodology V12n4(Oct 2003)pp371-408
 =IDEA TOOL MODEL CHECKING CTL FSM Kripke Multi-valued LOGIC Quasi-Boolean  Lattice \Chi\_CTL \Chi\_Check \Chi\_Kripke
 Extends classical {False, True} reasoning to {False, Maybe, True} values.  Good for incomplete models found during analysis.
 Able to have multi-valued variables in: state of FSM, Transitions between states, satisfaction.
 meaning(EX(p)) := backward_image(RR)(meaning(p)).
 backward_image(RR)(TT) := map[s:S](multivalued_union[t:T](TT(t) multivalued_intersection RR(s,t) )).
 Implementation described in 2002 CSRG Tech Report 446, University of Toronto
.Close

Cheek95
.Open Cheek95
 Martin Cheek
 Using Feedback to Improve Software Development
 IEEE Software Magazine V12n3(May 1995)pp89-90
 =REPORT FEAST EVOLUTION PEOPLE SYSTEMS
.Box
Reports on research by Manny Lehman<mml@doc.ic.ac.uk> - complex social interactions explains why 20 years of technological innovations do not correspond with a significan improvement in the development process.  The "Feast" Feedback Evolution And Software Technology.
.Close.Box
.Close

ChesnevarMaguitmanLoui00
.Open ChesnevarMaguitmanLoui00
    Carlos Ivan Chesnevar & Ana Gabriela Maguitman & Ronald Prescott Loui 
    Logical models of argument 
    ACM Computing Surveys V32n4(Dec 2000)pp337-383 
 =HISTORY 1950-99 FORMAL DIALECTIC DEFEASIBLE CONSISTENCY REASON ARGUMENT PLAUSIBLE AGENTS AI LAW NONMONOTONIC
 Formal logic is reasoning that can not be defeated. Normal reasoning is not like this.
 Detailed, difficult and hard to read.
 No ref to work on inconsistent requirements.  Small comment on OO inheritance.
.Close

Christy09
.Open Christy09
 Peter Christy
 Commentary: A Trip without a Roadmap
 ACM Queue V7n1(Mar 2009)
.See http://queue.acm.org/detail.cfm?id=1515746
 =CASE STUDY REVIEW TECHNOLOGY REQUIREMENTS RIA FITNESS PERFORMANCE USER
 Review of 
.See [Norwalk09]
 No user requirements -- straight to technological solution.  Performance an afterthought.
 Quote
.Box
A good start is to not imagine what users want or need, but instead to talk
with them about it. Try to walk in their shoes and understand how your 
software might help make their lives better (or not, as in this case). If 
you don't have time to do that yourself, then you should at least work with
good product marketing people and listen to what they have to say.
.Close.Box
.Close

ChungNixonYuMylopoulos99
.Open ChungNixonYuMylopoulos99
 Lawrence Chung & Brian A Nixon & Eric Yu & John Mylopoulos
 Non-functional Requirements in software engineering
 Kluwer Acad Norwell MA 2000 ISBN 0-7923-8666-3 QA76.758 .N65 1999
 =THEORY+CASESTUDYs  FORMAL NFR SOFTGOALS SIGs GRAPHICS TABLES LOGIC QUALITIES REALITIES SYSTEMS TECHNIQUES
 Accuracy, security, performance,
 SIG:= "Softgoal Independency Graph", pp17+48+85
  presenting arguments connecting statements independently of their (boolean) value: "dialectical style of reasoning".
 refinements and correlations
 {BREAK, HURT,  UNKNOWN, HELP, MAKE}, AND, OR, EQUAL.
 denied, undecided, satisficed.
 Consolidates and summarizes:
.See [MylopoulosChungNixon92]
.See [BorgidaMylopoulosReiter93]
.See [ChungNixonYuMylopoulos99]
.See [MylopoulosChungYu99]
.See [MylopoulosChungLiaoWangYu01]
also see
.See [Nixon00]
.Close

Church56
.Open Church56
 Alonzo Church
 Introduction to mathematical logic: Volume I
 Princeton Univ Press 1956 No17 in  Princeton mathematical series
 =TEXT LOGIC
 Skolem normal form in section 42 &43
.Close

CimattiRoveriSusiTonetta12
.Open CimattiRoveriSusiTonetta12
  Alessandro Cimatti & Marco Roveri & Angelo Susi & Stefano Tonetta
  Validation of Requirements for Hibrid Systems: A Formal Approach
 ACM TOSEM Trans Software Eng & Methodology V21n4(Nov 2012)#22:1-34
.See http://doi.acm.org/10.1145/2377656.2377657
  =CASE STUDY UML OTHELLO ETCS LTL LINEAR TIME LOGIC TRAINS TOOLS ROSE SMT WORD Requisite Pro
 UML used to describe domain, a natural language form of LTL.
 Requirements classified: Glossary, Relationship, Action, Configuration, Behavior, Scenario, Property, Annotation.
 Formalized as UML class diagram plus LTL logic constraints.
 Tools check for consistency and completeness of requirements.
 Discover unexpected scenarios and cases where unwanted behaviors are allowed by the requirements.
 Example constraint
	for all t in trains 
.( in the future t.front.end != t.MA.EOA.location and
.( in the future t.front.end = t.MA.EOA.location
.)
.)
 Experts learned to use the tools and method and liked them.
.Close

ClarkeEmersonSifakis09
.Open ClarkeEmersonSifakis09
 Edmund M Clarke & E Allen Emerson & Joseph Sifakis
 Model Checking: algorithmic verification and debugging
 Commun ACM V52n11(Nov 2009)pp75-84 
.See http://doi.acm.org/10.1145/1592761.1592781
 =HISTORY MODEL CHECKING LTL CTL CTL* MODAL LOGICS PROOF TOOLS 
 2007 Turing Prize Article
.Close

ClarkeGrumbergPeled99
.Open ClarkeGrumbergPeled99
 Edmund M Clarke Jr & Orna Grumberg & Doron A Peled
 Model Checking
 MIT Press 1999 ISBN 0-262-03270-8 QA 76.76 V47 C553 1999
 =MONOGRAPH FORMAL LOGIC CTL MODEL CHECKING SMV SPIN OBDDS KRIPKE SYMMETRY GROUPS
 CSUSB cs565/656
.Close

ClarkeRosenblum06
.Open ClarkeRosenblum06
 Lori A Clarke & David S Rosenblum 
 A Historical perspective on runtime assertion checking in Software Development
 ACM SIGSOFT Software Engineering Notes V31n3(May 2006)pp25-37
 =HISTORY ASSERTIONS LOGIC PROVING DEBUGGING Ada Eiffel Anna C++ Euclid
Turing 
 Excellent bibliography on pages 34-37
.Close

Cockburn96
.Open Cockburn96
 Alistair Cockburn
 The 3 Rings of Object Technology
 Object Magazine (Nov 1996) pp20-22
 DATA MODEL vs OBJECT-ORIENTED: structure vs changes. Modeling data on disk vs data in organization
 conceptual+logical+physical. Date model quicker. SCENARIOS:channel effort
 test completeness and variations. 
.See [CRC]
encourages creativity.
.Close

Cockburn02b
.Open Cockburn02b
  Alistair Cockburn
  Use Cases, ten years later
  STQE Magazine (Mar/Apr 2002)
.See http://alistair.cockburn.us/Use+cases,+ten+years+later
  =HISTORY =HOWTO USE CASES FORMALLITY Brief Casual Fully dressed STAKEHOLDERS GOALS    Theory
.Set
  Use cases about one type of user and their goals -- the Prime Actor.
  Use cases are about the user's goals and the ways they try to fulfill these.
Steps in scenarios achieve small goals on the way to a big goal.
And Goals have different scopes/levels/sizes.
  Because there are actions that are invisible to the Prime Actor there must be
other stakeholders involved with different interests.  
The Prime Actor want to get candy but the owner of the candy machine wants to get
money for the candy... So there are contracts that the system must follow.
 There is more value in thinking out the alternative scenarios than the main success
scenario.
.Close.Set
  How people reacted to use cases...
  Some peole like formal structured use cases but others dislike them.
 Advice: Keep them simple.  Keep them essential/logical.  Use multiple formats:
Brief, Casual, Fully Dressed.
 Mistakes: too many physical details, main use case too long and detailed.
.Close

CODASYL71
.Open CODASYL71
 CODASYL Database Task Group
 CODASYL Database Task Group report
 ACM  NY NY 1971
 =STANDARD data logic ENTITIES SETS(FUNCTIONS)
.Close

Coen-Porisinietal91
.Open Coen-Porisinietal91
 Alberto Coen-Porisini & Flavio De Paoli & Carlo Ghezzi & Dino Mandrioli
 Software Specialization Via Symbolic Execution 
 IEEE Trans SE-17 n9 (Sep 1991)pp884-899 CR9302-0092
 =DEMO logic symbolic execution re-engineering specialization
.Close

Cohen90
.Open Cohen90
 Jacqes Cohen
 Constraint Logic Programming Languages
 Commun ACM V33n7(Jul 1990)pp52-68
 =DEMO CLP non-sequential AI
.Close

CohenCampbell93
.Open CohenCampbell93
 Donald Cohen & Neil Campbell
 Automating Relational Operations on Data Structures
 IEEE Software Magazine(May 1993)pp53-59
Example: topological sort on page 54
.Box
 do( x' in graph & no y in graph(y before x);
      out:!x; graph:~x;
 )
.Close.Box
.Close

Colmerauer90
.Open Colmerauer90
 Alain Colmerauer
 An Introduction to Prolog III
 Commun ACM V33n7(Jul 1990)pp68-90
 =LRM logic-programming non-sequential AI
.Close

Conallen99
.Open Conallen99
 Jim Conallen(jconalle@Rational.com)
 Modeling web application architectures with UML
 Commun ACM V42n10(Oct 1999)pp63-70 in 
.See [Booch99]
 =ESSAY WWW/NET DESIGN  UML stereotypes vs 
.See [RMM]
 Also see 
.See [Conallen98]
on the WWW
 web application implement business logic and when accessed changes the state of the business. Separate business ADM from presentation UI.
 ADM:=Analysis/Design model
 classes: separate client side pages from server side pages.  serverside builds clientside.
 components: Iconic stereotypes
 stereotypes for: server pages, client pages, links,builds, form, parts of forms, frame, target, applets, javascript, activex,...
 Details to be announced
.See http://www.rational.com/
.Close

ContedeLeonAlves-Foss06
.Open ContedeLeonAlves-Foss06
 Daniel Conte de Leon & Jim Alves-Foss 
 Hidden implementation dependencies in high assurance and critical computing systems 
 IEEE Trans Software Engineering  V32n10(Oct 2006)pp790-811 
 =CASE STUDY FORMAL HA&CCS ARTIFACTS RELATIONS LOGIC PROLOG GRAPHIC IMPLEMENTATION ABSTRACTION GUAM DO-178B 
 Pedantic theory leads to tool that found problems in software from traceability relations on "work product sections" (artifacts).
 Translation into MATHS
.Net
 artifact:Sets.
 implements: @(artifact,artifact) =given, indicates traceability between artifacts.
 |-STRICT_ORDER(strict_relation=>implements, artifact).
 l: artifact>->level =given, assigns a level to each artifact.
 <: @(level, level) =given.
 |-STRICT_ORDER(strict_relation=>(<), level).
 dependency: @(artifact, artifact) =goal.
 d := dependency.
   |-  (conceptual_completeness):  for x, y, z: artifact((if (x  implements y and z) and l(x)<l(y)<l(z) then y d z) and (if (x and y  implements z) and l(x)<l(y)<l(z) then x d y))

STRICT_ORDER::=http://csci.csusb.edu/dick/maths/math_21_Order.html#STRICT_ORDER

.Close.Net
.Close

Cooke06
.Open Cooke06
 John Cooke 
 Constructing Correct software(2nd edn)
 Springer 2005  QA76.76  ISBN 1-85233-820-2
 =INTRODUCTION MATHEMATICS LOGIC PROOF CORRECTNESS PROGRAMMING TECHNICAL 
 compare with Bo Sandin's stuff in the 1980's and Huth & Ryan (textbook).
.Close

CookPodelskiRybalchenko11
.Open CookPodelskiRybalchenko11
 Byron Cook & Andreas Podelski & Andrey Rybalchenko
 Proving program termination  
 Commun ACM V54n5(May 2011)pp88-98
.See http://doi.acm.org/10.1145/1941487.1941509
 =DEMO MATHEMATICS TERMINATION LOGIC DISJUNCTIVE 
 Instead of proving that the transition relation R is a sub-relation of a well-founded relation T:
    R==>T,
One can try to prove that
    R^(1..*) ==> | [i:1..n] T[i],
where each T[i] is well-founded. 
 Claims that "Ramsey's Theorem" implies that only a finite collection of T's need be considered.
 Adding extra statements and assertions to the code can express termination as invariants. 
For example, to verify that a variable is decreasing but positive:
.As_is    assert( oldx > x && x > 0 );
.As_is    oldx:=x;    
 Tools can  then verify the invariants. 
 Compare Andreas Blass and Yuri Gurevich. ACM Trans Comp Logic (Dec 2006) pp1-25
.See http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.146.4485&rep=rep1&type=pdf
.Close

Cousot90
.Open Cousot90
 Patrick Cousot
 Methods and Logics for Proving Programs
 Chapter 15 (pp841..993) of Leeuwen90
 =THEORY Operational and relational semantics
.Box
Studies relation between operational and relational semantics. Theorem 
19(pages 856..858) proves that relational semantics imply operational with
termination ignored.  Angelic - Floyd non-determinsism and demonic - 
Dijkstra non-determinism being extreme cases in which operational can 
handle relational non-determinism.  Refers to HoareLauer84, GreifMeyer81
.Close.Box
.Close

Cowanetal95
.Open Cowanetal95
 Donald D Cowan & Carlos J P  Lucena
 Abstract Data Views: An Interface specification Concept to enhance Design for Reuse
 IEEE Trans on Software Eng VSE-21n3(Mar 1995)pp229-243 CR9602-0126
 =DEMO ADO ADV OBJECT-ORIENTED REUSE ARCHITECTURE
.Box
ADO - Abstract Data Object
Rediscovering the value of separating the physical from the logical and one type of object from another, also from network...
.As_is     I/O      ADO
.As_is        \     / ||
.As_is        ADV1    ADV2
MVC
suggests use of dynamic objects!

ADV2 are relations!

Claims OMT is an modernized version of JSD!(RUBBISH)

Quotes Kazman et al: Metaphors as first class objects.

Reccommends developing graphic notations
.Close.Box
.Close

CrowVito98
.Open CrowVito98
 Judith Crow & Ben Di Vito
 Formalizing Space Shuttle Software Requirements: Four CASE Studies
 ACM TOSEM V7n3(Jul 1998)pp215-249
 =ANALYSIS EXPERIENCE 
.See [PVS]
GPS RAPID FORMAL LOGIC TABLE MATH Mur\Phi
.Box
 Where do states come from, shared variables used as input/output.
 Large number of errors discovered (early) just by formalizing requirements without checking!
 Need for readymade math theories: eg properties of mappings!
 Failed proofs are more help than successful ones.
 Specification is iterative.
 Need to specify constraints found in the problem domain.
 Can simplify model: remove continuous values and time and remove costraints.
Therefore check some impossible states
 Tailor formal methods to the situation.
.Close.Box
.Close

DalaKamathKolarikSivaraman04 
.Open DalaKamathKolarikSivaraman04 
 Nikuni P Dala & Manjunath Kamath & WilliamJ Kolarik & Eswar Sivaraman
 Toward an Integrated Framework for Modeling Enterprise Process
 Commun ACM V47n3(Mar 2004)pp83-86
 =ADVERT BUSINESS PROCESS MODELLING  IMPROVEMENT ERP EPML XML Petri Analysis TED
 Need to model/implement distributed.
 Need for process semantics.
 Need to link business and enginering.
 Graphic front-end($EPML) <->XML<-> formal Back-end. Analise back end.
 NSF Scalable Enterprise Systems Initiative.
 EPML::="Enterprise Process Modelling Language".
 Graphic showing: activities (Human, Computer, Machine), logic and decision logic, data icons, control flows , (input, output)><( material, data),  timing triggers.
 TED::="Task Execution Diagram". 
Analysis petri nets: design (termination, deadlock, safety) + performance 
(resource assignment, simulation,  timing, success vs time statistics)
.Close

DanforthTomlinson88
.Open DanforthTomlinson88
 S Danforth & C Tomlinson
 Type Theories and Object Oriented Programming
 Comp Surveys  V20n1 (pp29-72)Mar 1988
 =THEORY object-oriented logic  Reality
.Close

Date00
.Open Date00
 Christopher J Date
 What not how: the business rules approach to application development
 Addison-Wesley Longman Boston MA 2000 pp131 $24.95 ISBN 0-201-70850-7 CR0011-0557 H.2.0 qa76.76 a65 d375 2000
 =ADVERT RULES SQL LOGIC LPC TABLES
.Close

DeBakker75
.Open DeBakker75
 J W de Bakker
 Flow of Control in the Proof of Sequential Programs
 Proc 16th Ann Symposium on the Fundamentals of Computer Science Berkeley California(pp29-33) IEEE Computer Society 1975
 =THEORY regular logic
.Close

DeganoEtAl08
.Open DeganoEtAl08
 Pierpaolo Degano & Rocco De Nicola & Jose Meseguer (eds) 
 Concurrency, Graphs and Models: Essays dedicated to Ugo Montanari on his 65th Birthday
 LNCS 5065 Springer Verlag Berlin Heidelberg (2008) $CR 0909-0812
 =FESTSHRIFT MATHEMATICS GRAPH THEORY CONCURRENCY NON-SEQUENTIAL CATEGORIES SEMIRINGS TOOLS HISTORY  
 Includes
.See [AstesianoReggioRicca08]
UML BUSINESS ...
.See [Baetan08]
ALGEBRA EQUATIONS AUTOMATA ...
.See [BeauxisPalamidessiValencia08]
NONSEQUENTIAL BAGS...
.See [HermenegildoEtAl08]
LANGUAGE Ciao ...
.See [Quaglia08]
BIOLOGICAL CELLULAR SYSTEMS...
.Close

Delgrande98
.Open Delgrande98
 James P Delgrande(Simon Fraser U, Burnaby, BC, Canada)<jim@cs.sfu.ca>
 On first-order conditional logics
 Artif Intell V105n1-2(Oct 1998)pp105-137 CR9903-0211
 =THEORY defeasible LOGIC possible worlds Kripke
.Box
 Proposes replacing `for all x( P implies_if_normal Q)` by `P implies_for_all_normal[x] Q`
 Examples: all birds fly, penguins are birds, penguins don't fly.
 All elephants like their keepers, unless the keeper is mean like Fred in which case they don't like him, unless the elephant is Clide who likes all the keepers.
.Close.Box
.Close

DeLine01
.Open DeLine01
 Robert DeLine
 Avoiding Packaging Mismatch with Flexible Packaging
 IEEE Trans Software Engineering  V27n2(Feb 2001)pp124-143  in ICSE'99
+ Correction IEEE Trans Software Engineering  V27n6(Jun 2001)p576
 =DEMO MODULE ARCHITECTURE ware+packager NONSEQUENTIAL
 Allows one piece of logic to be mapped into spreadsheet, CGI, yacc, ....
 Stresses use of coroutines as more flexible than procedural code.
.Close

DeMilloLiptonPerlis79
.Open DeMilloLiptonPerlis79
 Richard DeMillo & Richard Lipton & Alan Perlis
 Social processes and Proofs of Theorems and Programs
 Commun ACM V22n5(May 1979) pp271-280, letters V22n11pp621-630
 =ESSAY EXAMPLES MATHEMATICS PROOF LOGIC
 p272: "There is simply no way to describe the history of mathematical ideas without describing the successive social processes at work on proofs."
 See 
.See [Lakatos76]
.See [Bauer92]
 (DeMilloLiptonPerlis79)|- `rigorous software development will also depend on social processes`
.Close

DeMouraBjorner11
.Open DeMouraBjorner11
 Leonardo de Moura & Nikolaj BjC8rner
 Satisfiability modulo theories: introduction and applications
 Commun ACM V54n9(Sep 2011)pp69-77
.See http://doi.acm.org/10.1145/1995376.1995394
 =ADVERT LOGIC FORMAL MATHEMATICS PROBLEM SOLVING TOOLS SMT SAT 
 SMT solve problems within specialized mathematical theories. 
 Example theory: difference arithmetic where every formula has form `x-y<=c` where `x` & `y` are variables and `c` is a constant. 
 SMT work with SAT solvers. 
 Several solvers for different theories can be combined. 
 Many problems about programs can be expressed in the theories with tractable solvers. 
.Close

DeneckerBruynooghe02
.Open DeneckerBruynooghe02
 Marc Denecker & Maurice Bruynooghe
 Logic Programming Revisited: Logic Programs as Inductive Definitions
 ACM Trans Computational Logic V2n4(Oct 2001)pp623-654
 =THEORY LOGIC Prolog INDUCTION
.Close

Denning94
.Open Denning94
 Peter J Denning
 Designing a Discipline of Software Design
 Keynote address at the   7th SEI Conference on Software Engineering Education "Putting the 'Engineering' into Software Engineering" January 5-7 1994 San Antonio Texas USA
 =IDEA REALITY ONTOLOGY
.See [WandWeber90] cf
.See [WiederholdWegnerCeri93] cf
 ?? S-->RPQ->T (ontological mapping)
.Box
From Abstract

The central claim explored here is that the standard engineering design 
process produces a fundamental blindness to the domains of action in which
the customers of software systems live and work.  The connection between 
measurable properties of the software and the satisfaction of those 
customers is, at best, tenuous.  We propose a broader interpretation
of design that is centered on observing the work processes of a community 
of customers in a domain and connecting those processes to supportive 
software technologies.  The skill that a designer needs to have to observe
work processes and begin making the connections is here called 
`ontological mapping`.  This skill can be learned and is the basis of a discipline of 
software design.
.Close.Box
.Close

DenningHorning0202
.Open DenningHorning0202
 Peter J Denning & James J Horning
 Inside RISKS: Risks of Linear Thinking
 Commun ACM V45n2(Mar 2002)p120
 =ESSAY USER vs TECHNIQUE
 Quotes Donald Stokes (Pasteur's quadrant: basic science and technological innovation, Brooking's institute, 1997). 2><2: inspired by use >< quest for fundamental understanding. Pasteur(Y,Y), Bohr (N,Y), Edison(Y,N), and unnamed(N,N).
 Argues that software development is similar: focus on the user and focus on the technical aspects.
.Close

DesaiEtal05
.Open DesaiEtal05
 Nirmit Desai & Ashok  U Mallya & Amit K Chopra  & Munindar P Singh
 Interaction protocols as design abstractions for business processes
 IEEE Trans Software Engineering  V31n12(Dec 2005)pp1015-1027
 =THEORY MODEL BUSINESS PROCESS COMMITMENTS SCENARIOS OWL-P AGENTS ROLES \pi-CALCULUS
 Proposes a logic of commitments between agents.
 Uses sequence charts containing commitments to describe protocols.
 Implies that activity diagrams are a bad way to describe business processes.
Entangles the internal logic of different agents with each other.  So unstable.
 (dick)|- `take home message: don't use control flows to model work flow`.
.Close

DesaiChopraSingh09
.Open DesaiChopraSingh09
 Nirmilt Desai & Amit K Chopra & Munindar P Singh
 Amoeba: A methodology for modeling and evolving cross-organizational business processes 
 ACM Transactions on Software Engineering and Methodology V19n2(Oct 2009)pp6.1-45
 =ADVERT 2 CASE STUDIES Amoeba REQUIREMENTS METHOD LOGIC COMMITMENTS SCENARIOS SEQUENCE CHARTS AXIOMS EVOLUTION AGENTS SERVICES ORCHESTRATION CHOREOGRAPHY
 Amoeba::Method= iterate( roles and interactions; contractual relationships -> Commitments; message meanings->create and manipulate commitments; Constraints; compose protocols -> process model).
 Uses the idea of
.Key business protocols
as modules. These have messages and resulting changes in the commitments between components.
For example `CC(VENDOR, BUYER, pay(price), ship(goods))` would result from a VENDOR sending a 
`quotation(price, goods)` message to a BUYER.
 Theory
.See [DesaiEtal05]
.Close

Deville90
.Open Deville90
 Yves Deville
 Logic Programming: Systematic Program Development
 Addison Wesley 1990 QA76.63.D48 CR9204-0201 & CR9102-0042
 =TEXT LOGIC PROGRAMMING
.Box
Note
pp14-17 outlines steps: Problem->Spec(predicates, multiplicity and directionallity)->first order logic->logic program.

(MATHS suitable for expressing the Problem and perhaps the Spec as well.)

.Close.Box
.Close

Dijkstra76
.Open Dijkstra76
 Edsger W Dijkstra
 A Discipline of Programming
 Prentice Hall Inc Englewood Cliffs NJ
 =TEXT guarded-commands sequential non-sequential formal logic structures
.Close

Dijkstra89
.Open Dijkstra89
 Edsger W Dijkstra
 On the Cruelty of Really Teaching Computer Science
 Talk at ACM Computer Science Conference Louisville  Feb 1989(See 
.See [Denning89b]
)
 =TALK formal logic education
.Close

DilligDilligAiken10
.Open DilligDilligAiken10
 Isil Dillig & Thomas Dillig & Alex Aiken
 Reasoning about the unknown in static analysis
 Commun ACM V53n8(Aug 2010)pp116-123
.See http://doi.acm.org/10.1145/1787234.1787259
 =DEMO LOGIC MATHEMATICS MODEL CHECKING C Linux may/must SOUNDNESS 
.Close

Dillonetal94
.Open Dillonetal94
 Laura K Dillon & G Kutty & L E Moser & P M Melliar-Smith && Y S Ramakrishna
 A Graphical Interval Logic for Specifying Concurrent Systems
 ACM Trans Softw Eng Methodol V3n2(Apr 1994)pp131-165
.See http://citeseer.nj.nec.com/33145.html
.See http://portal.acm.org/citation.cfm?id=192218.192226&coll=portal&dl=ACM&idx=J790&part=transaction&WantType=transaction&title=ACM%20Transactions%20on%20Software%20Engineering%20and%20Methodology%20%28TOSEM%29&CFID=1643654&CFTOKEN=8691090

 =ADVERT NOTATION MODAL TEMPORAL LOGIC FORMAL GIL TOOL GILED
 GIL::="Graphic Interval Logic".
 Later see 
.See [RTGIL]
-- real time GIL
.Close

DjuricDevedzic10
.Open DjuricDevedzic10
 Dragan Djuric & Vladan  Devedzic
 Magic Potion: incorporating new development paradigms through metaprogramming
 IEEE Software Magazine V27n5(Sep/Oct 2010)pp38-44
 =ADVERT JAVA LISP JVM Modeling Spaces XML RDF/OWL DSL DOMAIN MODEL LOGIC ONTOLOGY UML MDA
Clojure::=http://clojure.org,
Dialect of LISP that runs in the Java Virtual Machine.
.Close

Doernhoefer06a
.Open Doernhoefer06a
 Mark Doernhoefer
 Surfing the Net for Software Engineering Notes: Requirements Management
 ACM SIGSOFT Software Engineering Notes V31n2(Mar 2006)pp17-25
.See  http://doi.acm.org/10.1145/1118537.1118553
 =SURVEY NET REQUIREMENTS
 Excellent survey of resources on the web
.See http://www.jiludwig.com/
.See http://cio.doe.gov/ITReform/sqse/requirements_management.htm
.See http://www.goldpractices.com/practices/mr/index.php
.See http://www.sei.cmu.edu/str/descriptions/reqtracing.html
.See http://www.agilealliance.com/articles/AgileArticlesCatSearch?category=Requirements
.See http://www.paper-review.com/tools/rms/read.php
(tools)
.See http://www.opengroup.org/architecture/togaf8-doc/arch/p2/p2_req.htm
.See http://www.rallydev.com/life_cycle_management.jsp
.See http://www.erequirements.com/app?service=page/Methodology
.See http://www-306.ibm.com/software/rational/offerings/reqanalysis.html
.See http://www.telelogic.com/
.See http://www.iceincusa.com/16CSP/content/8_requir/reqfrm.htm
plus lots more...
.Close

Doernhoefer09c
.Open Doernhoefer09c
 Mark Doernhoefer
 Surfing the net for software engineering notes: computer science
 ACM SIGSOFT SEN V34n5(Sep 2009)pp8-17
.See http://doi.acm.org/10.1145/1598732.1598752
 =SURVEY SWEBOK SigACT ALGORITHMS CALGO NUMERICAL NIST GAMS DATA STRUCTURES THEORY HARDWARE TM OS IMBOK FUZZY LOGIC PROGRAMMING LANGUAGES 
.Close

Douglass99
.Open Douglass99
 Bruce Powel Douglass
 Components: Logical, Physical Models
 Software Development Magazine V7n12(Dec 1999)pp52-54
 =ADVERT OBJECT-ORIENTED METHOD UML ROPES COMPONENTS
 Components are runtime plugin Binaries not objects
.Note UML components include data files, web pages, source code, etc etc.
.Close

DutertreStavidou97
.Open DutertreStavidou97
 Bruno Dutertre & Victoria Stavidou
 Formal Requirements Analysis of an Avionics Control System
 IEEE Trans Softw Eng VSE23n5(May 1997)pp267-278
 =DEMO V&V REQUIREMENTS LOGIC TOOLS TIMING RISKS REALITY PVS
.See [PVS]
 model of time and clocks
 exposed some unstated assumptions about REALITY and one defect
.Close

DuvalHodgins06
.Open DuvalHodgins06
 Erik Duval & Wayne Hodgins  
 Standardized Uniqueness: Oxymoron or Vision  of the Future
 IEEE Computer Magazine  V39n3(Mar 2006)pp96-98
 =STANDARD EDUCATIONAL OBJECTS METADATA LOM IEEE1484 LTSC XML
 The IEEE1484 standard specifies the information to be recorded about "Learning Objects":  artifacts that help you learn.
 The standard is  MODULAR separating logical structure from physical bindings.
 The standard defines many data elements in a hierarchical data model but every part is optional.
 How to make the metadata invisible?
.Close

EdwardsJacksonTorlak04
.Open EdwardsJacksonTorlak04
 Jonathan Edwards & Daniel Jackson & Emina Torlak 
 A Type System for Object Models
 Proc SIGSOFT'04/FSE-12& ACM SIGSOFT Software Engineering Notes V29n6(Nov 2004)pp189-199
 =IDEA LOGIC RELATIONAL TYPES Alloy 2.0
 Defines an improved type system for Alloy with subtypes, relations, etc.
 Compares with  UML OCL.
 Precisely defines two types for formulas: bounding type and relevance type.
 An empty relevance type indicates an error.
.Close

Eisenstadt97
.Open Eisenstadt97
 Marc Eisenstadt
 My Hairiest Bug War Stories
 Comm ACM V40n4(Apr 1997)pp30-37 CR9711-0918
 =POLL RISKS QUALITIES DEBUGGING
 Very interesting.
 Internet POLL for bugs classified for difficulties(long cause-effect chain and hampered tools being commonest) + how found(gathered data and ispeculation leading) + root cause(memory, vendor, design,logic, initialization
...) +interaction(use data gathering when cause-effect chain is likely to be long or the tools are hampered)
.Close

EmmerichEtal99
.Open EmmerichEtal99
 Wolfgang Emmerich & Anthony Finkelstein & Carlo Montangero & Stefano Antonelli & Stephen Armitage & Richard Stevens
 Managing Standards Compliance
 IEEE Trans Software Engineering V25n6(Nov/Dec 1999)pp836-837
 =THEORY MODEL  LOGIC FLEA TOOL DOORS DXL STANDARDS in PROCESS
 uses STATECHART UML~OCL+1st_order_logic PETRI Net LISP (AP5)
 FLEA::="Formal Language for Expressing Assumptions".
.Close

Engelsetal92
.Open Engelsetal92
 G Engels & C Lewerentz & M Nagl & W Schafer & A Schurr
 Building Integrated S Development Environments Part 1: Tool Specification
 ACM Trans Softw Eng Methodol  V1n2(Apr 1992)pp135-167
.Box
IPSEN(Integrated Project Support Environment) PROGRESS Attributed Graphs visual data base CFG+CS rules on attributes in graph, object oriented is-a, prime as new node, Path expressions, atomic transactions, Factoring out common  rules, logical vs representation graph.

.Close.Box
.Close

Epstein94
.Open Epstein94
 Richard L Epstein
 The Semantic Foundations of Logic: Predicate Logic
 Oxford U Press Inc NY NY ISBN 0-19-508760-7 CR9601-0018
 philosophical translation of Natural language into various predicate calculi
.Close

Epstein01a
.Open Epstein01a
 Richard L Epstein
 Predicate logic: The semantic foundation of Logic
 Wadsworth Belmont CA 2001 ISBN 0-534-55846-1 BC181.E67 2001 $40.95 pp412 CR0011-0555 F.4.1
 =TEXT =REFERENCE LOGIC PC MODAL 
 `x is a dog` notation! 
 CSUSB CS556/656
.See [Epstein94]
.Close

Epstein01b
.Open Epstein01b
 Richard L Epstein
 Propositional logic: The semantic foundation of Logic
 Wadsworth Belmont CA 2001 ISBN 0-534-55846-1 BC181.E67 2001b
 =TEXT =REFERENCE LOGIC PC MODAL 
 CSUSB CS556/656
.Close

Epstein06
.Open Epstein06
 Richard L Epstein
 Classical mathematical logic: The semantic foundation of Logic
 Princeton UP Princeton NJ 2006 ISBN 0691123004 $CR 0803-0245
 =UNREAD =TEXT =REFERENCE LOGIC
 Compare
.See [Epstein01b]
.See [Epstein01a]
.See [Epstein94]
.Close

Farmer03
.Open Farmer03
 William M Farmer
 A Basic Extended Simple Type Theory
 McMaster University Hamilton Ontario CA (29 Sep 2003)
 =IDEA LOGIC TYPES 
 BESTT ::= $CSTT with HOL, sets, lists, & tuples. 
CSTT ::= Church's Simple Type  Theory.
.Close

FarmerMohrenschildt00
.Open FarmerMohrenschildt00
 William M. Farmer and Martin v. Mohrenschildt
 Transformers for Symbolic Computation and Formal Deduction
 Presented at a Workshop on the Role of Automated Deduction in Mathematics,
CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 2000
.See http://imps.mcmaster.ca/doc/transformers.pdf
 =IDEA LOGIC DEDUCTION COMPUTATION TERM TRANSFORMERS
 STTM::="von-Neumann-Bernays-Goedel set theory".
This has terms and formulas. Terms may be undefined, but formulas are always defined
and are either true or false.
 Transformers are total functions which may or may not preserve meaning or logistic properties like being (provably) true or false.
.Close

Felderetal94a
.Open Felderetal94a
 Miguel Felder & Dino Mandroli & Angelo Morzenti
 Proving Properties of Real-Time Systems Through Logical Specifications and Petri Nets
 IEEE Trans SE V20n2(Feb 1994)pp127-141
 =FORMAL TIMING Temporal TRIO
.Box
Basic temporal operator
  Dist( P, d ) ::=`P is true d time units from (_)`,
 model of timed petrie nets
 proof that dining philosphers TPN  is deterministic and every body eats every 7 units of time!

compare with MATHS manual on Modal Logic

Question: They prove a liveness property of the philosophers by proving a liveness property for one fork.  Is this circular?
.Close.Box
.Close

Felderetal94b
.Open Felderetal94b
 Miguel Felder  & Angelo Morzenti
 Validating Real-Time systems by History-Checking TRIO Specifications
 Trans Softw Eng Methodol V9n4(Oct 1994)pp308-339
 =EXPERIENCE TIMING TRIO LOGIC SPECIFICATION PROOF
.Box
Some experiences with Italian utility companies

Semantic tableaus for proof and for history checking

 Futr(A,t) ::=A(_+t), Past(A,t) ::=A(_-t)
 Table 1, p316 defines:
   AlwF, AlwP, Alw, SomF, SomP, Som,Lats,Lasted, since, Since[w], WithinP, Until, Until[w], UpToNow, FirstTimeF
.Close.Box
.Close

FeltyNamjoshi03
.Open FeltyNamjoshi03
 Amy P Felty & Kedar S Namjoshi
 Feature Specification and automated Conflict Detection
 ACM TOSEM Trans Software Eng & Methodology V12n1(Jan 2003)pp3-27
 =CASESTUDY telecommunications  SPECIFICATION FEATURES LOGIC LTL FSM Buchi MODEL Checking TOOL FIX COSPAN
 Features expressed in sugared LTL: pre/post conditions. including until/unless discharge requirements.
 Complex/careful definition of what it means for two features to conflict.
 FIX use LTL approximation to find witnesses  for conflicts.
.Close

FerrariGnesiMontanariPistore03
.Open FerrariGnesiMontanariPistore03
 Gian-Luigi Ferrari & Stefania Gnesi & Ugo Montanari & Marco Pistore
 A Model-Checking Verification Environment for mobile Processes
 ACM TOSEM Trans Software Eng & Methodology V12n4(Oct 2003)pp440-473
 =DEMO TOOL MODEL CHECKING MOBILE \pi-calculus FSM HD-Automata HAL \pi-logic ACTL 
.Close

FeysFitch69
.Open FeysFitch69
 RObert Feys & Frederic B Fitch
 Dictionary of Symbols of Mathematical Logic
 Amsterdam North-holland Pub Co 1969
 =DICTIONARY LOGIC SYMBOLISM LANGUAGE
.Close

FilipenkoMorris92
.Open FilipenkoMorris92
 I Filipenko &  F L Morris
 Domains for Logic Programming
 Theor Comput Sci V94n1(Mar 1992)pp63-99
 CR9304-0239"Original and sound"
.Close

Finkelsteinetal94
.Open Finkelsteinetal94
 Anthony C W Finckelstein & Dov Gavey & Anthony Hunter & Jeff Kramer & Bashar Nuseibeh
 Inconsistency Handling in Multiperspective Specifications
 IEEE trans on Soft Eng vSE-20n8(Aug 1994)pp569-578
 =IDEA REQUIREMENTS LOGIC SPECIFICATION See Nuseibehetal94
.Box
VeiwPoint::=Net{Style, Work_Plan, Domain, Specification, Work_Record}.
.Close.Box
.Close

Firesmith93
.Open Firesmith93
 Donald G. Firesmith
 Object-oriented Requirements analysis and logical design: A software engineering approach
 John Wiley & sons NY NY 1993 ISBN 0-471-57807-X CR9502-0058
.Close

FittingMendelsohn98
.Open FittingMendelsohn98
 Melvin C. Fitting and Richard Mendelsohn
 First-Order Modal Logic
 Kluwer 1998 paperback 1999
 =TEXT FORMAL LOGIC MODAL THEORY
 Modal predicate logic
.Close

Floyd67a
.Open Floyd67a
 Robert W Floyd
 Assigning Meaning to Programs
 pp19-32 of Proceedings of Symposia in Applied Mathematics Vol XIX
 formal logic PROOF
.Close

Fowler01c
.Open Fowler01c
 Martin Fowler
 Separating User Interface code
 IEEE Software Magazine V18n2(Mar/Apr 2000)pp96-97
 =ESSAY MODULES USER REALITY XML SQL HTML
 p.96: ` Separate presentation code from domain code.`
 increases maintainability, portability, testing.
 Problems: VB, Delphi,... don't do this.  WEB server pages that contain business logic.
 HTML vs XML.
.Close

Fox66
.Open Fox66
 Fox(Ed)
 Advances in Programming & Non-Numerical Computation
 Pergamon Press Oxford UK
 =SURVEY formal logic
.Close

Francez86
.Open Francez86
 Nissim Francez
 Fairness
 Springer Verlag NY NY 1986(Texts & Monographs in Comp Sci). ISBN 0-387-96235-2
 (UCR) QA76.6.F7226
 ACM(D.1.3 D.2.4 D.3.1 D.4.1 F.1.2 F.3.1 F.3.3)
 termination safety liveness temporal logic
.Close

Fraseretal94
.Open Fraseretal94
 Martin D Fraser & Kuldeep Kumar & Vijay K Vaishnavi
 Strategies for Incorporating Formal Specifications in Software Develpment
 Commun ACM V37n10(Oct 1994)pp74-86 CR9509-0705
.Box
Note -- quotes examples limitted to VDM+XYZ
Footnote 1: Specification in terms of system components, options,...  vs Spec as callection of user's "functional requirements"
p75: past research has focussed on notation and rules of inference not on methods and tools, "The Softaware engineer is lef to his or her own devices to discover the software requiements and structure them into a requirements architecture."
p75: Most need discrete math and logic which most SwEngs don't know.

Table 1
 Page77: defines methods, lists 10: VDM, Z, Larch, FSM, Petri Nets, Temporal Logic, Transition Axioms, CSP, CCS, PAISLEY
 Page 78.  Lists 9 strategies of use
Table 2, page 79: informal vs semi-formal vs formal: definition and examples (JSD as semiformal)
Morphological analysis
Table 3: Formalization Processes (taxonomy= { direct, transitional={sequential, parallel}})
Table 4: Support: Unassistted vs Computer Assisted
Table 5: Table 3 >< Table 4 -> references

25 refs
.Close.Box
.Close

Freedman83
.Open Freedman83
 Roy S Freedman
 The Common Sense of Object Oriented Languages
 Computer Design pp111-118
 structures object-oriented logic
.Close

FreydScedrov89
.Open FreydScedrov89
 Pete J Freyd & Andre Scedrov
 Categories& Allegories
 Elsevier Amsterdam Netherlands ISBN0-444-70368-3 QA169.F73
 allegories are abstracted from binary relations like categories abstracted from functions
 notation for diagrams: noncommuting (+) + pullbacks + equalizers + products
 quantification based on making visible the comments(quantiviers and logical connectives) made while drawing the diagram on a blackboard
.Close

FriasEtal05
.Open FriasEtal05
 Marcello F Frias & Carlos G Lopez Pombo & Gabriel A Baum & Nazareno M Aguirre & Thomas S E Maibaum
 Reasoning about static and dynamic properties in Alloy: A Purely Relational Approach
 ACM TOSEM Trans Software Eng & Methodology V14n4(Oct 2005)pp478-526
 =THEORY EQUATION RELATIONAL LOGIC HOARE TRIPLES FORK ALGEBRA FRL
 A
.Key fork algebra
is based on a set that has a pairing operation (`p`) that is used to define a `fork` operation on relations:
  fork ::infix=map[R,S] rel[a,d](for some b,c (d=p(b,c) and a R b and a S c)).
.Close

GanterWille99
.Open GanterWille99
 Bernhard Ganter & Rudolf Wille R
 Formal concept analysis: Mathematical foundations
 Springer 1999 QA171.5 G3513 1999
 =THEORY MATHEMATICAL FORMAL LOGIC LATTICE CONCEPT 
 Given a set of objects X, a set of attributes Y, and a relation R:@(X><Y),
then (X,Y,R) is called a formal context. If A is a subset of X then define
A'={y:Y. for all x:A(x R y)}.  Similarly B'={x:X.for all y:B( x R y)}. A 
formal concept is a pair (A, B) where A'=B and B'=A, and A is the extent and
B the intent of concept (A,B).  The subconcept_superconcept relation:(A1,B1)
<= (A2,B2) iff A1 is a subset of A2.  This defines  a lattice of formal 
concepts.
  Leads to a diagram showing the underlying structure of the relation R.
  Given a table X><Y<>-> Z and by defining a scaling Z into (true, false) then a context can be defined.
 See
.See http:://www/dick/maths/logic_42_Properties_of_Relation.html
for some rough notes on Concept analysis.
 Note.  Theory has been used to aid the maintenance of software: 

.See [BojicVelasevic00]

.See [DeursenKuipers99]

.See [LindigSnelting97]

.See [SiffReps99]

.See [Snelting96]

.See [SneltingTip98]
.Close

GaoHayesCai05
.Open GaoHayesCai05
 Hong Tina Gao & Jane Huffman Hayes & Henry Cai
 Integrating Biological Research through Web Services
 IEEE Computer Magazine  V38n3(Mar 2005)pp26-31
 =DEMO WEB SERVICES BIOINFORMATICS Drug discovery
 Combine many remote components to analyze data.
 Need standards.
 Helps if people split Model from View.
.Close

Garfinkel05
.Open Garfinkel05
 Simson Garfinkel
 Microsoft's Secret Bug Squasher
 Wired  (Nov 10 2005)
.See http://www.wired.com/news/technology/bugs/0,2924,69375,00.html?tw=wn_tophead_3
 =REPORT MS MODEL CHECKING DEVICE DRIVERS TOOL SLAM
 So called `formal methods` -- math & logic -- are used inside Microsoft!
.Close

GargantiniMorzenti01
.Open GargantiniMorzenti01
 Angelo Gargantini & angelo Morzenti 
Automated Deductive Requirements analysis of Critical systems
 ACM TOSEM Trans Software Engineering & Methodology V10n3(Jul 2001)pp255-307
 =DEMO FORMAL REQUIREMENTS ANALYSIS  SRA  LOGIC 
.See [TRIO]
TD TOOL  PVS Non-Zeno
 TD:="Time dependent".
 TRIO -- see Federer
 DUC::="Device under Construction".
 events (point based predicates) : true at a single time and not immediately before or after.
 interval-Based predicates: if true then true in some before or after interval nearby and if false then false nearby..
 left and right closed interval-based predicates and variables.  Left continuous interval based (lci) means that predicate has the same value at a given time as it had in a previous neighboring interval.
  non-Zeno predicates and variable.  Named after Zeno's paradoxes.   finite variability. physical meaningful.  One can talk about the value immediately before or after the current time.
 non_Zeno(A) ::=(UpToNow(not A) or UpToNow(A)) and (NowOn(not A) NowOn(A) ),
 UpToNow(A) ::= t+>for some d1>0, all d2:(0..d1) ( A (t-d2)),
 NowOn(A) ::= t+>for some d1>0, all d2:(0..d1) ( A (t+d2))
.Close

GeethaSubramanian90
.Open GeethaSubramanian90
 T V Geetha & R K Subramanian
 Representing Natural Language with Prolog
 IEEE Software V7n2 pp85-92
 =ADVERT DDD LOGIC PROLOG LANGUAGE NLP
.Close

GervasiNuseibeh02
.Open GervasiNuseibeh02
  Vincenzo Gervasi & Bashar Nuseibeh
   Lightweight validation of natural language requirements 
 Software - Practice & Experience V32n2(Feb 2002)pp113-133
 =CASESTUDY LITE FORMAL V&V REQUIREMENTS LOGIC NASA
 Shows how lightweight formalism can find errors in natural language specifications.
 This is easy and not expensive, and finds subtle errors.
.Close

GiannakopoulouMagee03
.Open GiannakopoulouMagee03
 Dimitra Giannakopoulou & Jeff Magee
 Fluent Model Checking for Event-based systems
 FSE-11 & ESEC 9 & ACM SIGSOFT Software Engineering Notes V28n5(Sep 2003)pp257-266
 =THEORY TOOL TEMPORAL LOGIC V&V LTS LTL FLUENT FLTL LTSA Buchi
 A fluent is a property of states defined by events at the start and end.  Example TUNING starts when the tuner is turned on and ceases when the device is tuned in.
 Syntax: <start_set, end_set> initially (true|false).
 Define shorthand for fluents for single actions/sets of actions: <S, All~S>initially false.
.Close

Gilb96
.Open Gilb96
 Tom Gilb(gilb@acm.org)
 Level 6: Why we Can't Get There From Here
 IEEE Software Magazine V13n1(Jan 1996)pp97-98+103
 =ADVERT QUALITY evolutionary delivery engineering Softcrafters
.Box
Quotes Biily Koen(U of Austin TX) : "Engineering is the use of principles to find designs that will meet multiple competing objectives within limited resources and other constraints, under conditions of uncertainty".

Platitudes instead of quantitive specs make engineering logically impossible.
.Close.Box
.Close

GilmoreTsiknis93
.Open GilmoreTsiknis93
 Paul C Gilmore & George K Tsiknis(UBC)
 A Logic for Category Theory
 Theor Comput Sci V111n1-2(Apr 1993)pp211-252
 CR9409-0647
.Box
CR(T H Tse) : Natural deduction based set theoretic semantics for categories - using joint denial and universal quantification as primitive... Tarski semantics... categories & Functiors... avoids paradoxes but permits selfmembership (eg category of categories is a category!)...remarkable.  some doubts.
.Close.Box
.Close

GortonLiuBrebner03
.Open GortonLiuBrebner03
 Ian Gorton & Anna Liu & Paul Brebner 
 Rigorous Evaluation of COTS Middleware Technology
 IEEE Computer Magazine V36n3(Mar 2003)pp50-55
 =DEMO QUALITIES WEB/NET Java J2EE servers MTE WebSphere WebLogic ...
.Close

Gries91
.Open Gries91
 David Gries
 Teaching Calculation and Discrimination: A More Effective Curriculum
 Commun ACMV34n3(Nar 1991)pp44-54. Letters Commun ACM V34n9(Oct 1991)pp16-18 & 91-95 & Commun ACM V35n2(Feb 1992)pp22-26
 =ESSAY FORMAL LOGIC MATH EDUCATION
.Box
text book version 
.See [GriesSchneider93]

p45"In Summary, Software engineering, Computing, and Computing education all suffer from a lack of basic mathematical skills that are needed in dealing with algorithmic concepts.", "Calculational proofs", "overhauling the CS Magor",
 p54"The main activity that is supposed to separate engineering from other fields is design: the actual activity of preparing a plans for some object[..] design of proofs[...]".
 p54"Let us all learn more about calculational techniques and gain skill with them: and let us begin to teach computing using them."
.Close.Box
.Close

Gries96
.Open Gries96
 David Gries(mailto:gries@cs.cornell.edu)
 The Need for Education in Useful Formal Logic
 IEEE Computer Magazine V29N4(Apr 1996)pp29-30
.Box
Logic as a tool.

calculational proofs


logic is a tool not a panacea
.Close.Box
.Close

GriesSchneider95
.Open GriesSchneider95
 David Gries &  Fred B Schneider
 Teaching Math More Effecively Through Calculational Proofs
 Am Math Monthly V102n8(Oct 1995)pp691-697)
 =ADVERT CALCULATIONAL LOGIC MATHEMATICS
 Advert for
.See [GriesSchneider93]
.Box
 15 axioms and 4 rules
 = is transitive, can substitute a free variable,
 equanimity:
	if P and (P \equiv Q) then Q
 and Liebnitz:
.Box
	E[v:=P]
	=     <P=Q>
	E[v:=Q]
.Close.Box
Where P and Q are expressions and v some variable not found in P or Q and E[v:=P] some expression with every ovccurrence of v replaced by P and E[v:=Q] the same expression with every v replaced by Q.

Also treats \equiv as an associative (serial) operator, and equals as a parallel operator.

Unified notation for all quantification, summation,  etc:
  (op var | condition : expression)

Formal notation is a repository of facts and a means of clarification.  It provides rules for judging the soundness of inference and detecting and eliminating ambiguity.
.Close.Box
.Close

Grossman11
.Open Grossman11
 Lisa Grossman
 Study: Math Skills Rely on Language, Not Just Logic
 Wired Science (Feb 8 2011)
.See http://www.wired.com/wiredscience/2011/02/homesigning-numbers/
 =REPORT EXPERIMENT SIGNERS NUMBERS COUNTING ARITHMETIC PEOPLE PSYCHOLOGY
 This reports on a recent experiment in Nicuagua by Elizabet Spaepen.
It shows that if you don't know the words for the numbers
you can not communicate a number (as in the number of sheep) correctly.
 Memorizing the mnemonic sequence (one,two, three, ...) provides pegs to hang
observations on...
.Close

Grunske08
.Open Grunske08
 L Grunske
 Specification patterns for probabilistic quality properties
 ACM/IEEE 30th Conf ICSE'08 Software Engineering(May 2008)pp31-40
 =THEORY =DEMO PROBABILISTIC VERIFICATION QUALITIES PCTL* CSL TEMPORAL LOGIC ProProST PATTERN LANGUAGE STRUCTURED ENGLISH GRAMMAR
 English Subset
.See ./samples/Grunske08.html
grammar.
.Close

Guerevich87
.Open Guerevich87
 Yuri Guerevich
 Logic and the Challenge of Computer Science
 pp1-57 in Borger88
.Box
Note "For years formal languages were in the private domain of logicians. 
But what formal language is most popular today?[...] The most popular 
formal languages are programming languages. Another kind of popular formal
languages are database query languages. Some other formal languages emerge
in artificial intelligence like languages for knowledge representation. Old
discussions on names, denotations, types, etc. are suddenly revitalised to
unprecedented magnitude"(p1),"no first order formula \phi expresses on 
finite graphs that (x,y) belongs to the transitive closure of the edge 
relation"(pp3-4).
.Close.Box
.Close

Gumb89
.Open Gumb89
 Raymond D Gumb
 Programming Logics: An Introduction to Verification and Semantics
 John Wiley & Sons NY NY 1989
 natural deduction
 introduction to hoare axioms and dentational semantics
.Close

Gurevich88
.Open Gurevich88
 Yuri Gurevich
 Logic and The challenge of Computer Science
 in 
.See [borger88]
 =THEORY FORMAL LOGIC COMPUTING
.Close

GurfinkelDevereuxChechik02
.Open GurfinkelDevereuxChechik02
 Arie Gurfinkel & Benet Devereux & Marsha Chechik
 Model Exploration with temporal logic query checking
 SIGSOFT 2002/FSE 10 & ACM SIGSOFT Software Engineering Notes V27n6(Nov 2002)pp139-148
 =DEMO TOOL MODEL CHECKING CTL QUERIES
 Given a finite state model enable the faster answering of questions like:  what property is always true with `p`.
 Cruise control example.
  refers to Chan's original idea.
 Developed to 
.See [GurfinkelChechikDevereux03]
.Close

GurfinkelChechikDevereux03
.Open GurfinkelChechikDevereux03
 Arie Gurfinkel & Marsha Chechik & Benet Devereux
 Temporal Logic Query Checking: A Tool for Model exploration
 IEEE Trans Software Engineering  V29n10(Oct 2003)pp898-914
 Based on 
.See [GurfinkelDevereuxChechik02]
 =IDEA MODAL TEMPORAL LOGIC CTL Placeholders DeMorgan Algebra TLQSolver \chi\_Chek Cruise control SCR CSCI656
 Instead of checking a CTL for truth/falsity: compute the formula that "fill in the blanks" in a CTL formula:
 AG(?1) -- what is always and forever true?
  AX(?1{p,q}) -- what formula on p and q (only) is always true in the next step?
 AG(?1 /\ AX?2) -- what pair of formulas ...
.Close

Guzdial95
.Open Guzdial95
 Mark Guzdial<guzdial@cc.gatech.edu>
 Centralized Mindset: A student Problem with Object-Oriented Programming
 Papers of the 26th SIGCSE Tech Symposium on CS Ed SIGCSE Bulletin V27n1(Mar 1995)pp182-185
 =EDUCATION PEOPLE OBJECT-ORIENTED vs FUNCTIONAL
 Tendency for students to pack all the logic and structure into a single 
leader object rather than use communcation and shared responsibillity.  
 Claims result is less reusable.
 Solutions: Motivate, evaluate alternatives, teach class library, provide experience
.Close

HaleyLaneyMoffettNuseibeh08
.Open HaleyLaneyMoffettNuseibeh08
 Charles B Haley & Robert Laney & Jonathon Moffett & Bashar Nuseibeh 
 Security Requirements engineering: A Framework for Representation and Analysis
 IEEE Trans Software Engineering  V34n1(Jan/Feb 2008)pp133-153
 =CASESTUDY SECURITY REQUIREMENTS METHOD  
 Describes a complex process and set of languages that work from security goals, to assets that are to be protected
(compare
.See [Stoneburner06]
), to requirements, thence to arguments for a particular system design satisfying the requirements, and so to the assumptions that can be rebutted, and the mitigation of the rebuttals and so forth.
 Security requirements are non-functional requirements and are closely related to the context of the machine being designed.
 Must expose assumptions about the machine and its context.
 Arguments that the system satisfies the requirements lead to lists of assumptions that can be challenged (WHY?) and rebutted.
 Rebuttals lead to mitigators that change the context and/or the requirments.
In turn the mitigators can be rebutted, and so on.
 Hence an iterative process making the design more secure.
 Uses Jackson Problem Frames
(
.See [Jackson95c]
.See [Jackson01]
), simplified
.See [Toulmin79]
arguments, Propositional logic, and a causal logic based on
 `Event1` shall cause `Event2`.
 Outer_argument::=`Formal logic showing the design satisfies the requirement and exposing assumptions`
 Inner_argument::=`Explores assumptions in terms of rebuttals and mitigators`.
 Process involves engineers and stakeholders in intense and fruitful discussion.
 (dick)|- Compare
.See [Lakatos76]
model of the mathematical process.  Also methods used to achieve safety.
.Close

HalleVillemaireCherkoui09
.Open HalleVillemaireCherkoui09
 Sylvain Halle & Roger Villemaire & Omar Cherkaoui
 Specifying and validating data-aware temporal web service properties
 IEEE Trans Software Engineering V35n5(Sep/Oct 2009)pp669-683
 =THEORY TOOL LANGUAGE TEMPORAL LOGIC DATA WEB SERVICES CTL-FO+ PSPACE-complete PROOF
.Close

HalleVillemaireCherkoui09
.Close

HalpernZuck92
.Open HalpernZuck92
 Joseph Y Halpern & Lenore D Zuck
 A Little Knowledge Goes a Long Way: Knowledge-Based Derivations and Correctness Proofs for a Family of Protocols
 J. ACM V39n3(Jul 1992)pp449-478 
.See [CR]
(Oct 1993)
 =THEORY PROVING REFINEMENT PROTOCOLS KNOWLEDGE MODAL LOGIC
 Argues for the high level design of inefficient solutions that can be shown to be 100% correct and then their refinement into efficient solutions that implement th high level ones.
 Derives the Alternating Bit Protocol and Stenning's protocol for the Sequence Transmission problem.
 Defines data flow and how to implement it using unreliable communication.  Safety: output sequence is prefix of input sequence. Liveness: all inputs are ultimately output (given fairness).
.Close

Hamilton01
.Open Hamilton01
 Scott Hamilton
 Formalizing Concept Maps
 IEEE Computer Magazine V34n1(Jan 2001)pp66+68 (Figure and Side-bar)
 =IDEA GRAPHIC LOGIC MODEL RKF USER vs FORMAL
 RKF := Rapid Knowledge Formation.
 Concept maps are informal concept graphs or semantic nets.
.Close

HanEtal00a
.Open HanEtal00a
 Yan Ha n & Xu Chun-gen & Zhang Gong-xuan & Liu Feng-yu
 Constraint specification for object model of access coontrol based on role
 ACM SIGSOFT Software Engineering notes V25n2(Mar 2000)pp60-64
 =PATTERN FORMAL UML LOGIC
 Dynamic roles form a hierarchy
.Close

HannaM93
.Open HannaM93
 Mary Hanna
 Reengineering aims for Legacy Salvation
 IEEE Software Magazine (Sep 1993)p41-48
 =POLL ENGINEERING TOOLS REQUIREMENTS
.Box
MIS Wish List (p41) (all in 4..5 on a 1..6 scale)
 1. Capture data defintions
 2. Identify problem code
 3. Support Version Control
 4. Capture Data Models
 5. Analyze data flows and logic
 6. Capture process model

 Usage(p42)
 debug, Test, change management
 pp44-45+47: Table of 79 vendors selling reeng tools!
.Close.Box
.Close

HansenRavnRischel91
.Open HansenRavnRischel91
 Kirsten M Hansen & Anders P Ravn & Hans Rischel
 Specifying and Verifying Requirements of Real Time Systems
 ACM SIGSOFT'91 Conf on Software for Critical Systems: Software Eng Notes V16n5(Dec 1991)pp44-54
 republished IEEE Trans SE-19n1(Jan 1993)pp41-55
 =DEMO TIMING REALITY Requirements SYSTEM LOGIC
.Box
 "1. An application domain system model of the equipment and its intended environment of use is defined.  This is a dynamic system model, and defines the overall states of the system as functions of time.  Requirements are constraints on this model." 2. control model 3. design model. Interval logic(predicates define durations of states) formal
.Close.Box
.Close

Harel79
.Open Harel79
 David Harel
 First Order Dynamic Logic
 Springer Verlag 1979 (PhD Thesis MIT 78)
 =THESIS regular logic structure
.Close

HarelKozenTiuryn00
.Open HarelKozenTiuryn00
David Harel & Dexter Kozen & Jerzy Tiuryn
 Dynamic Logic
 MIT Press 2000 ISBN 0-262-08289-6 $50 QA76.9 L63 H37
  =TEXT LOGIC TEMPORAL
 for cs565/656
.Close

Hares90
.Open Hares90
 John S Hares
 SSADM for the Advanced Practitioner
 John Wiley & Sons NY NY 1990
 =TEXT SSADM
Content
.Box
 1 Past and future
 2 strengths and weaknesses
 3. Pearls of PRactical Wisdom
 4 Distributed, Realtime, Conversational
 5 Expert Systems & Object Oriented Design
.List
  OOD
    Normalize logic as well as attributes.
    access paths ---> responsibillity clusters
.Close.Box
.Close

Hart95
.Open Hart95
 Johnson M. Hart
 Experience with Logical Code Analysis in Software Maintenance
 Software Practice and Experience V25n11(Nov 1995)pp1243-1262
 =DEMO EXPERIENCE PROOF
.Box
jon@bilbo.radonc.washington.edu, Jon Jacky at University of Washington:

The
author used simple reasoning about weakest preconditions,
postconditions, invariants and logic to find and fix errors in real C
code for TCP/IP and other communications software.  A nice example of
a pragmatic use of formal methods for program derivation and verification.
.Close.Box
.Close

HawkinsEtAl12
.Open HawkinsEtAl12
  Peter Hawkins & Martin Rinard & Alex Aiken & Mooly Sagiv & Kathleen Fisher
  An introduction to data representation synthesis
  Commun ACM V55n12(Dec 2012)pp91-99
.See http://doi.acm.org/10.1145/2380656.2380677
  =TOOL RelC COMPILES RELATIONAL DATA to STRUCTURES HASH LIST VECTOR PERFORMANCE 
 Method:=relational TNF data; logical queries; physical data structures; physical queries;  code; performance. 
 Essentially an implementation of Keith Robinson's data design theory from 1980 SSADM! 
.Close

HavelunddLowryPenix01
.Open HavelunddLowryPenix01
 Klaus Havelundd & Mike Lowry & John Penix
 Formal analysis of a Space-Craft Controller using SPIN
 IEEE Trans Software Engineering  V27n8(Aug 2001)pp749-765
 =CASESTUDY FORMAL MODEL CHECKING TOOL SPIN LISP LTLMODAL LOGIC  ESL PROMELA
 Deep Space 1.
 Located a major design flaw.
 found a bug that testing missed that caused problem 98M kilometers from Earth.
 LTL::="Linear Temporal Logic", properties of traces using modes  [] = always and <> meaning some.
 Interviewed programmer about impact of work: `found difficult mission-killing bugs -- thought formal meant program proving not finding bugs`.
.Close

HayAtlee00
.Open HayAtlee00
 Jonathan D hay &  Joanne M Atlee
 Composing Features and resolving Interactions
 
.See [FSE8]
pp110-119
 =CASESTUDY FORMAL EVOLUTION CVF LOGIC Relations POTS
 A way to add features to a complex system even when they conflict with the system and each other.
.Close

HayesB05
.Open HayesB05
 Brian Hayes
 Naming Names
 American Scientist V93 (Jan/Feb 2005)
and republished in
.See [HayesB08]
 =ARTICLE CODING DATA
.List
 Internet account IDs
 NY Stock Exchange Ticker Symbols -- up to 3 Uppercase letters -- 26+26**2+26**3 possible
 Universal Product Codes -- bar codes -- (
.Key UPC
)-- 12-digit until January 2005, and then 13-digits.
 Global Traded Item Numbers (GTIN)
 European Article Numbers (EAN)
 Biological Species -- Two Latin-like words
 The Chemical Elements -- One uppercase letter + option lower case letter.
(I had to program these while working for ICI in the 1960's)
 Organic Chemicals -- Complex coding.
 Internet Assigned Number Authority 
.Key IANA
names for countries -- two ASCII letters
 Radio Call Signs -- 3..4 Capital letters -- KVCR, KFROG, ...
 Telephone numbers -- 10 digits (in the USA).
 Social Security Numbers -- 9 digits in the USA
 Airport codes (IATA) -- Three letters.
 Names of Horses -- 2..18 characters  ( letters plus space, period, and apostrophe).
.Close.List
.Close

Hayes09
.Open Hayes09
 Brian Hayes
 Writing Math on the Web
 American Scientist V97n2(Mar-Apr 2009)pp98-102
 =ARTICLE HTML \TeX TeX MathML JsMath FONTS techexplorer
 Problems with putting formulae onto web pages.
 Where to render the formula: author, server, or client?  
 Client: Plugin(techexplorer), fonts, special script (JsMath).
Rely on user having the plugins and fonts to work.
 Server example -- Wikipedia uses `texvc`, MathTeX, MimeTeX. All make graphic images.
reliable and ugly.
 How to render:  as a graphical image or using Fonts or Unicode?
 Failure of MathML to become mainstream.
 (dick)|-Failure of \TeX to express hypertext markup.
 (dick)|- No formal syntax and semantics for proofs and logic in \TeX or MathML
 (dick)|- Still like my $MATHS language better.
.Close

HazzanDubinsky08
.Open HazzanDubinsky08
 Orit Hazzan & Yael Dubinsky
 Agile Software Engineering
 Springer Pub NY NY(2008) ISBN 184001983 $CR 0912-1151
 =MANUAL PEOPLE AGILE TEAMS TESTS REFLECTION HUMAN ORGANIZATIONAL TECHNOLOGY
 HOT::analysis=Human >< Organizational><Technological.
 Describes a process that helps people learn what might be taught directly in other books.
 Not clear if they are training students or teachers.
 The treatment of refactoring is completely inadequate.
.Close

Hehner84a
.Open Hehner84a
 Eric C R Hehner
 Predicative Programming Part I
 Commun ACM V27N2 ( Feb 1984)pp134-151
 =DEMO dynamic logic regular
 Next part
.See [Hehner84b]
.Close

Hehner84b
.Open Hehner84b
 Eric C R Hehner
 Predicative Programming Part II
 Commun ACM  V27n3( Mar 1984)
 =DEMO dynamic logic regular non-sequential
 Follows
.See [Hehner84a]
.Close

Heitmeyer02
.Open Heitmeyer02
 Constance Heitmeyer
 Software Cost Reduction   
 Center for High Assurance Computer Systems (CHACS) Publications 2002
.See http://chacs.nrl.navy.mil/publications/CHACS/2002/2002heitmeyer-encse.pdf
 =HISTORY PARNAS NRL SCR IDEAS NOTATIONS TOOLS TABULAR LOGIC NAT IN OUT REQ  A-7E TAME  REQUIREMENTS DESIGN MODULES
 @T(c) ::=`c becomes true`,
 @F(c)::=`c becomes false`.
 SCR uses logic and tables to express very clearly what is expected of a new system.
 Software that monitors certain inputs and controls certain outputs.
 It uses a four variable model (NAT+REQ+IN+OUT) that distinguishes 
the assumed properties (NAT) from the requirements (REQ).
IN and OUT specify tolerances.
 Software has `modes`.  Tables relate modes and events.  Finite State model.
 Human inspection for defects proved expensive and tools uncovered more defects afterwards.
 Tools include SPIN, TAME, PVS, Salsa, an invariant generator, .
 Usable subsets of requirements lead to the `uses hierarchy`,  `module guide`, etc..
 Methods and tools applied to real projects to discover problems. 
 Also see
.See [HeitmeyerEtal98]
.See [HeitmeyerKirbyLabaw97]
.Close

Heitmeyer02a
.Open Heitmeyer02a
 Constance Heitmeyer
 Software Cost Reduction. 
 Article in 
.See [Marciniak02]
 =UNREAD =HISTORY PARNAS NRL SCR IDEAS NOTATIONS TOOLS TABULAR LOGIC NAT IN OUT REQ  A-7E TAME  REQUIREMENTS DESIGN MODULES
 Compare
.See [Heitmeyer02]
perhaps
.Hole Heitmeyer02a
.Close

Hennessy88
.Open Hennessy88
 ?? Hennessy
 Algebraic Theory of Processes
 MIT Press MA 1988
 =TEXT ALGEBRA MATH NONSEQUENTIAL logic
.Close

HenryFaller95
.Open HenryFaller95
 Emmannuel Henry & Benoit Faller
 Large-scale Industrial Reuse to Reduce Cost and Cycle Time
 IEEE Software Magazine V12n5(Sep 1995)pp47-53
 =EXPERIENCE C++ TECHNICAL REUSE COST PROCESS
.Box
Note sizes 400...500KLOC of C++ EXPERIENCE
Separated physical, GUI, Data comms, data base and logic of a naval permanent system
and could then reuse the physical,GUI.... parts in an mobile army system

significant speed up in delivery, productivity and 30% decraes in the number of faults/LOC.

Also used incremental delivery to validate and improve GUI.

Claims that there is much to be said for starting out with reusing what you have on the way to developing a new process.

Use of good design, and C++.  Design elements are about 20 classes. functional set(subsystem has 30..100 design elements).

Reuse 20..50%, faults down 15%..50% as well.
.Close.Box
.Close

HermenegildoEtAl08
.Open HermenegildoEtAl08
 M V Hermenegildo & F Bueno & N Carro & P Lopez & J F Morales & G Puebla 
 An Overview of the Ciao Multiparadigm Language and Program Development Environment and its Design Philosophy
 Montanari Festschrift  pp208-237
.See [DeganoEtAl08]
 =ADVERT LANGUAGE Ciao TOOL THEORY FUNCTIONAL OO LOGIC CONSTRAINT 
 Downloads
.See http://www.ciaohome.org
.See http://www.cliplab.org
.See mailto:ciao@clip.dia.fi.upm.es
 91 references 
.Close

Hersh95
.Open Hersh95
 Ruben Hersh
 Fresh Breezes in the philosophy of Mathematics
 American Math Monthly V102n7(aug-sep 1995)pp589-594
 =HISTORY MATHEMATICAL LOGIC
.Box
logicism, formalism, intuitionism have produced no solutions to the question of why math works as well as it does.

Compares history to the philosophy of science:
Phil/Sc went thru a logical positivist phase of (axioms, maps, theories) 
before people studied what real scientists do...

Humanistic ideas about math: human, fallible, rigor varies, empirical clues
and numerical experiments and probabilities help more than logic, objects 
as social-cultural-historical objects

p593: "Study of the lawful, predictable parts of the physical world has a 
name. That name is 'physics'.  Study of the lawful, predictable parts of 
the social-conceptual world has a name.  The name is 'mathematics'."
.Close.Box
 Compare 
.See [Lakatos76].
.Close

HincheyEtAl08
.Open HincheyEtAl08
 MIke Hinchey & Michael A Jackson & Patrick Cousot & Byron Cook & Jonathen  P Bowen & Tiziana 
 Software Engineering and Formal Methods
 Commun ACM V51n9(Sep 2008)pp54-59 
.See http://doi.acm.org/10.1145/1378727.1378742
$CR 0908-0760
 =SURVEY FORMAL MATHEMATICAL LOGICAL METHODS TOOLS QUALITIES RELIABLE COST 
 Summary of three key note speeches from ICSE&FM 2007.
 Describes history:  increasing dependability of hardware, more intensive use of software,  more ubiquitous computing, no increase in software dependability.
  Formal methods can increase dependability.
 Jackson notes that good engineering stays within the
.Key normal design discipline
associated with a given application domain.
.Key Radical design
leaves the normal and always decreases the dependability of the result.
Therefore the need to develop special purpose disciplines for each domain.
Refers to
.See [Vincenti90]
on engineering.  
Compare with Henry Petrosky's work.
 Patrick Cousot defines formal methods and the idea of abstraction. Mentions Astree.
 Byron Cook notes the explosion of complexity when there is concurrency and the attempts to overcome it.
 Conclusion reviews the history, describes
.Key method engineering
and states that the quest continues...
.Close

Hoare69
.Open Hoare69
 C.A.R. Hoare
 An Axiomatic Basis for Computer Programming
 Commun ACM V12 n10 Oct 69
 =THEORY logic formal structures
.Close

Hoare78
.Open Hoare78
 C.A.R. Hoare
 Communicating Sequential Processes
 Commun ACM v21 n8 pp666-677(Also book -See 
.See [Hoare85]
)
 =THEORY non-sequential logic CSP
 Contrast
.See [Milner80]
CCS
.See [Baetan90]
ACP
.Close

Hoare85
.Open Hoare85
 C.A.R. Hoare
 Communicating Sequential Processes
 Prentice Hall 1985
 =IDEA CSP non-sequential formal logic structures
 Developed from
.See [Hoare78]
 Contrast
.See [Milner80]
.See [Baetan90]
ACP
 Later edition(2006) online
.See http://www.usingcsp.com/cspbook.pdf
as PDF.
.Close

Hoare09
.Open Hoare09
 C A Hoare
 retrospective: an axiomatic basis for computer programming
 Commun ACM V52n10(Oct 2009)pp30-32 
.See http://doi.acm.org/10.1145/1562764.1562779
 =HISTORY VERIFICATION PROGRAMMING LOGIC PROOFS TESTS HACKERS SPECIFICATIONS COSTS
 Looking back at
.See [Hoare69]
40 years later.
Compare
.See [Hoare01]
 Expected to retire before research was complete and industry adopted methods.
 Surprised to find "assert" in C/C++.
 Didn't expect the new logics/mathematics that have been developed.  
 Tests test the programmer not the program.
 Hackers have got industry interested in verification -- finally.  
 Academic and industrial research should complement each other. One goes for the big ideals  and the other for low hanging fruit.  
 Reply
.See Humelsine10
(letter).
.Close

Hoareetal87
.Open Hoareetal87
 C.A.R. Hoare & IJ Hayes & HE Jifeng & CC Morgan &AW Roscoe & JW Sanders & IH Sorenson & JM Spivey & BA Sufrin
 Laws of Programming
 Commun ACM V30n8 (pp672-686)1987
 =IDEA formal sequential logic
 For practicing engineers mathematical laws are also more relevant than the
elaborate models constructed in a study of foundations.
 could define programs as relations that are total and with images that are
either finite or else universal with fictitious "state at infinity" for 
non-termination.
 finite texts have a normal form ignoring speed.
.Close

HoareBroySteinbruggen01
.Open HoareBroySteinbruggen01
 Tony Hoare & Manfred Broy & Ralf Steinbruggen
 Engineering theories of Software Construction
 IOS Press(2001) Amsterdam, The Netherlands ISBN 1586031724 CR 0304-0310
 =WORKSHOP ENGINEERING MATH LOGIC MODELING PROBLEM-FRAMES REALITY REACTIVE Petri 
.Close

Hodges77
.Open Hodges77
 Wilfrid Hodges
 Logic
 Penguin Books Middlesex UK & NY NY 1977
 =TEXT FORMAL LOGIC Semantic Tableaux TREEs
 Describes an easy to learn and use method of proving/disproving results.
 Compare with earlier
.See [Jeffrey67]
and next edition
.See [Hodeges05]
.Close

Hodges05
.Open Hodges05
 Wilfred Hodges
 An Introduction to Elementary Logic, Second Edition
$20.00 Paperback | 5.07 x 7.79in | 304 pages | ISBN 9780141003146 | 28 Dec 2005 | Penguin UK
 =TEXT FORMAL LOGIC Semantic Tableaux TREEs
 Describes an easy to learn and use method of proving/disproving results.
 Based on earlier
.See [Jeffrey67]
.Close

Hoffman08b
.Open Hoffman08b
 Leah Hoffman
 Talking Model-checking Technology
 =INTERVIEW HISTORY MODEL CHECKING VERIFICATION FSM TEMPORAL LOGIC 
 Commun ACM V51n7(Jul 2008)pp112+110-111 
 Interview with Turing prize winners E Allen Emerson & Edmund M Clark & Joseph Sifakis
 Painful birth: theoretically trivial and practically impossible!
 Handle programs that do not stop.
Avoid humans proving programs.
Based on finite state abstractions of program+hardware and requirements specified in temporal logic.
If property is not satisfied by abstraction then procedure gives a diagnostic trace of the bad behavior.
 Problem: State Explosion: no of cases to consider can grow exponentially with the size of the model.
 Benefits: precise specifications.
 Limits: 10^100 states!
 Microsoft has one used for device drivers!
.Close

HoffmanWeiss01
.Open HoffmanWeiss01
 Daniel M Hoffman & David M Weiss
 Software fundamentals: Collected Papers by David L Parnas
 Addison-Wesley 2001 CR0109-0914 ISBN 0-201-70369-6 QA76.754P36
 =COLLECTION REQUIREMENTS MODULES DESIGN LOGIC TECHNICAL SCR TABULAR  LANGUAGES METHODS SDI A7 ENGINEERING
.Close

Holloway95
.Open Holloway95
 C Michael Hollowy<c.m.holloway@larc.nasa.gov>
 Software Engineering epistomology
 ACM SIGSOFT Software Engineering Notes V20n2(Apr 1995)pp20-21
 =SURVEY LOGIC FALACIES PROCESS IMPROVEMENT
How do we know that something is true:
.Box
Authority
  Divine -> Absolute truth
  Human -> Opinion

Reason
  Logic -> Conditional Absolute Truth

Experience
  Anedotal Experience -> Possible truth
  Experimental Experience -> Probable truth

Pronouncements with little logic or experiemne.

Resistance to data collection in projects
....
.Close.Box
.Close

HollowayButler96
.Open HollowayButler96
 C Michael Hollowy<c.m.holloway@larc.nasa.gov> & Ricky W Butler
 Impediments to Industrial Use of Formal Methods
 IEEE Computer Magazine V29N4(Apr 1996)pp25-26
 =EXPERIENCE FORMAL METHODS
.Box
NASA Langley Research center spnsoring industrial projects: AAMP-FV processor, toold manipulating decision tables.

showed impediments: tools, examples, expectations that tools sell themselves.
 Tools: "Not only do the input languages use specialized notations from mathematical logic, but many tools have numerous bugs in them.  Few things are more disconcerting..."  need to improve quality of current not their power.
 Examples are toy, interesting but irrelevnt
 The first effort in a new domain requires far greater creativity than subsequent efforts.

need to provide guidance for executives  on matching method to applications. unbiased assessments.
.Close.Box
.Close

Holzmann02
.Open Holzmann02
 Gerard J. Holzmann
 The Logic of Bugs
 SIGSOFT 2002/FSE 10 & ACM SIGSOFT Software Engineering Notes V27n6(Nov 2002)pp81-87
 online at
.See http://doi.acm.org/10.1145/587051.587064 
 =Keynote BUGS V&V SQA MODEL CHECKING TOOLS NOTATIONS LOGIC GRAPHIC  LTL SPIN TimeLineEditor
  Human fallibility: abut 12 errors in 13800 sentences in a typical NYTimes.  Careful programmers have similar error rates(?).
 Argues that bugs evolve:  the mutate and only some type survive.
 The weakest point is where the bugs are to be found.
 The weak point in model checking is the language used to specify requirements.
 Suggests using a graphic notation instead of a temporal logic.
.Close

Honidenetal94
.Open Honidenetal94
 Shinichi Honiden & Kazuhiko Nishimura & Naoshi Uchihira & Kiyoshi Itoh
 An Application of Artificial Intelligence to Object-Oriented Performance Design (OOPD) for Real-Time Systems
 IEEE Trans SE VSE-20n11(Nov 1994)pp849-867
 =DEMO LOGIC NONDECLARATIVE OBJECT-ORIENTED PROLOG MENDEL
 Automatic redesign of lift controler to avoid bottleneck
.Close

Horrocks08
.Open Horrocks08
 Ian Horrocks 
 Ontologies and the Semantic Web
 Commun ACM V51n12(Dec 2008)pp58-67
.See http://doi.acm.org/10.1145/1490360.1409377
 =POPULARIZATION WEB ONTOLOGIES SEMANTICS LOGIC  RULES RDF OWL 
 Figure 2:the
.Key Tree of Porphyry
.See http://en.wikipedia.org/wiki/Tree_of_Porphyry
(Wikipedia) and
.See ./maths/http://csci.csusb.edu/dick/maths/logic_8_Natural_Language.html#Stuff
(MATHS)
 RDF expresses labelled directed graphs: subject --(verb)--> Object.
What we used to call semantic nets in the 1970s.
.Close

HouHoover06
.Open HouHoover06
 Danqing Hou & H James Hoover 
 Using SCL to Specify and check Design Intent in Source Code
 IEEE Trans Software Engineering  V32n6(Jun 2006)pp404-423
 =CASESTUDY TOOL V&V SQA STATIC CHECK TECHNICAL CODE Java C++ MVC   
 SCL::="Logic based language and tool that expresses and checks constraints on object-oriented code" 
 Typical constraint: In Java all classes derived from Object should define a `public boolean equals(Object o) method`, not one with another parameter type.
 Lint for the 21st century.
.Close

Humby73
.Open Humby73
 E Humby
 Programs from Desion Tables
 Macdonald London UK & American Elsevier NY NY 1973 ISBN 0-356-04126-3 & 0-444-195969-6 respectively LCCard#72-90803
 =HANDBOOK Tables SQA REQUIREMENTS QUALITY COMPLETENESS AMBIGUITY implementation COBOL
 A 
.Key Decision Table
is an early non-procedural and non-language description of requirements and logic.
They can be translated into code.
Manually they where difficult to maintain.
 They are a table with two parts.  First come the conditions -- one per row
and then come the actions.
 Each condition can (in a simple decision table) have one of two values: T or F.
The columns indicate T, F, and - (either).
In the actions an X indicates an action to be done and a - one that is not done
(we can also use A,B,C, ... in a column to indicate the sequence of actions.
 Example Decision table from page 88
.Table Labels	Rules	1	2	3	4
.Row C1	He knows	N	N	Y	Y
.Row C2	He knows C1	N	Y	N	Y
.Row A1	Shun him	X	-	-	-
.Row A2	Teach him	-	X	-	-
.Row A3	Wake him	-	-	X	-
.Row A4	Follow him	-	-	-	X
.Close.Table
.Close

Humphrey95a
.Open Humphrey95a
 Watts S Humphrey (SEI)
 A Discipline for Software Engineering
 Addison-Wesley Redwood City CA 1995 (SEI Series in software Engineering)
 ISBN 0-201-54610-8 BNB 93-41673 QA76.758H857
 =TEXT PSP IMPROVEMENT ESTIMATION METRICS
.Box
PSP=Personal Software Process

(ac)|- Did not work well as CS455(Software Engineering) text.

Includes logic and statistics! Goal-Question-Metric.
Tables("Templates") in chapter 10 "software design".

See 
.See [Humphrey95b]
for quick summary.

Reviewed by Tom DeMarco: revolutionary idea that individuals should be
responsible for estimation and measurement, not institutions.   Weakest in
low-level design. IEEE Computing Magazine  Oct 1995 pp82-83

Follow ups: Textbook on PSP: 
.See [Humphrey97;]
the Team Software Process(
.See [TSP]
),
introduction 
.See [Humphrey00]
.Close.Box
.Close

HuntbachRingwood95
.Open HuntbachRingwood95
 Mathew M Huntbach & Graem A Ringwood
 Programming in Concurrent Logic Languages
 IEEE Software Magazine(Nov 1995)pp71-82
 =PAPER TECHNICAL NONSEQUENTIAL  vs NONDETERMINISM BACKTRACKING PERFORMANCE
 adding paralelism efficiently means redefining nondeterminism and so abandoning backtracking with result that is not logic programming
.Close

HunterNuseibeh97
.Open HunterNuseibeh97
 Anthony Hunter & Bashar Nuseibeh
 Analysing Inconsistent Specifications
.See [RE'97] pp78-86
 =FORMAL REQUIREMENTS LOGIC
 REQUIREMENTS LOGIC must not include `ex falso quodlibet` and should track all inferences from stated requirements to conclusions and so aid diagnosis of inconsistencies
 QC::="Quasi Classical Logic"
.Close

HunterNuseibeh99
.Open HunterNuseibeh99
 Anthony Hunter & Bashar Nuseibeh
 Managing Inconsistent specifications: Reasoning, Analysis, and Action
 ACM ToSEM V7n4(May 1999)pp335-367
 =IDEA labelled QC Quine FORMAL LOGIC SPECIFICATION
 Label requirements and record deductions so that you can back track when
inconsistent ones emerge.
.See [QC]
 Compare with the way mathematicians handle inconsistencies in
.See [Lakatos76].
 (dick)|- my MATHS notation uses
.As_is 		(reason, reason, ...)|-(label): statement.
to record such connections but does not allow the same freedom
in abandonning and adjusting the logic.
.Close

HuthRyan00
.Open HuthRyan00
 Michael R Huth & Mark Ryan
 Logic in Computer Science: Modeling and reasoning about systems
 Cambridge U P 2000 ISBN 0 521 65200 6 (hardback) ISBN 0 521 65200 8 (paperback)
 =TEXT FORMAL MODEL LPC MODAL LOGIC CTL OBDDs AGENTS VERIFICATION SMV CSUSB.CSCI556/656
.Close

JacksonD00
.Open JacksonD00
 Daniel Jackson
 Automating first-Order Relational Logic
 
.See [FSE8]
pp120-139
 =THEORY LOGIC RELATIONS PREDICATE Z OCL =DEMO TOOL 50KLOC Java SAT Alloy Analyzer Nitpick UML COM
Mobile IP
 Shorter than SMV by 10 times.
 Quantifiers make logic easier to use. Analysis s faster than Nitpick as well.
 Describes syntax, type rules and semantics of the logic.
 In place of composition of relations ( R; S = rel[x,z](some y, x R y S z)), defines navigation ( R . S = rel[x,z](some y, y R z and y S x))
 scalar variables are replaced by singleton set variables.
 analysis:= normalize and skolemize; boolean formula; conjunctive normal form; SAT solver; map back to relational.
 Alloy_Analyzer::=http://sdg.lcs.mit.edu/alloy
 Proved UML meta-model is consistent in less than 20 seconds.
 See also 
.See [JacksonDSullivan00]
.Close

JacksonD02
.Open JacksonD02
 Daniel Jackson
 Alloy: A Lightweight Object Modeling Notation
 ACM TOSEM Trans Software Eng & Methodology V11n2(Apr 2002)pp256-290
 =IDEA GRAPHIC FORMAL  Object-Oriented  NOTATION Alloy Z SEMANTICS LOGIC SETS RELATIONS FUNCTIONS
.Close

JacksonD06a
.Open JacksonD06a
 Daniel Jackson
 Software Abstractions: Logic, Language, and Analysis
 The MIT Press Cambridge MA 2006 ISBN 0262101149 $CR 0802-0116 0806-0536
, rev edn 2012 ISBN 0262017156 $CR 1211-1092 1212-1193
 =TEXT Alloy LIGHT FORMAL MODEL CHECKING METHODS TOOLS
 A neat way of finding bugs in specifications and requirements.
 Small_scope_hypothesis::=`Most bugs have small counterexamples`.
 Notes the difficulty of creating consistent formal models that
have the desired properties.
 Alloy::language=`a formal first order relational logic expressed in ASCII with tools in Java`.
 Alloy_examples::=http://softwareabstractions.org.
 Alloy_analyzer::=http://alloy.mit.edu.
.Close

JacksonDShlyakhterSridharan01
.Open JacksonDShlyakhterSridharan01
 Daniel Jackson & Ilya Shlyakhter & Manu Sridharan
 A Micromodularity Mechanism
 ACM SIGSOFT proc ESEC-8 FSE-9 Software Engineering Notes V26n5(Sep 2001)pp62-73
 =IDEA MODULAR SPECIFICATIONS RELATIONS FORMAL NOTATION LOGIC EXTENSION TOOL? cf Z Alloy
 On the WWW
.See http://sdg.lcs.mit.edu/~dnj/publications
 |- A structure is a set of atoms and its fields are global relations that map atoms to other sets of atoms.
 |- Structure extensions are just subsets.
    sig name [parameters] extends parent[parameters]{ field: associate ...}{properties}:  field is a relation between name and associate and name is a subset of parent. 
    fact { property }: makes assumptions, states constraints, can retrofit fields
    assert{properties}: theorems -- properties that are intended to hold, and so need checking.
    fun name(para:type...){property}: defines properties that may or may not be true.  used to describe methods, abstraction.
 Simpler and more focused than Z, VDM, or MATHS
.Close

JacksonVaziri00
.Open JacksonVaziri00
 Daniel Jackson & Mandana Vaziri
 Finding Bugs with a Constraint Solver
 Proc ISSTA 00 & ACM SIGSOFT Software Engineering Notes V25n5(Sep 2000)pp14-25
 =DEMO LOGIC Alloy disproving
 find scope limited models of (Pre and Code and nou Post )
 Programs with pointers often have errors exposed in seconds. Worst  6 minutes.
.Close

Jacquet93
.Open Jacquet93
 Jean-Marie Jacquet
 Constructing Logic Programs
 John Wiley & Sons NY NY 1993
 ISBN 0-471-93789-4 CR9601-0007(D.1.6)
 skeletons + links to OO
.Close

JaspanEtAl09
.Open JaspanEtAl09
 Ciera Jaspan & Michael Keeling & Larry Maccherone & Gabriel L. Zenarosa & Mary Shaw 
 Software mythbusters explore formal methods
 IEEE Software Magazine V26n6(Nov/Dec 2009)pp60-63
 =REPORT DISCUSSION EXPERIENCE MYTHS FORMAL METHODS AGILE FSM LOGIC MATHEMATICS
 Reference a list
.See [Hall90]
of seven myths
 Formal methods are richer than in 1990.
 They are now used in requirements to get precision and understanding.  
They are embedded in tools and environments reducing the need for mathematical maturity. 
 They enable communication and evolution and so support agility. 
 An FSM model for understanding lead to better code. 
 Must match the method to the problem cost-effectively.
 Formal methods are being domesticated.   
.Close

Jeffrey67
.Open Jeffrey67
 Richard C Jeffrey
 Formal Logic: Its Scope and Limits
 McGraw-Hill NY NY 1967
 =TEXT FORMAL LOGIC semantic Tableaus TREES
 An easy to use way of proving things.
 Compare with the later
.See [Hodges77]
and
.See [Jeffrey91]
.Close

Jeffrey91
.Open Jeffrey91
 Richard C Jeffrey (Princeton U)
 Formal Logic: Its Scope and Limits
 McGraw-Hill Higher Education NY NY 1991 ISBN 0-07-032357-7
 =TEXT FORMAL LOGIC semantic Tableaus TREES
 An easy to use way of proving things.
 Improved edition of
.See [Jeffrey67].
 Compare with the earlier
.See [Hodges77]
.Close

JonesCB95
.Open JonesCB95
 Cliff B Jones
 Partial Functions and Logics: A Warning
 IPL V54n2(??? 1995)pp65-67
 =THEORY FORMAL LOGIC
 See 
.See [LPT]
 and 
.See [LPV]
.Close

JonesJones91
.Open JonesJones91
 Peter C Jones & Paul E Jones Jr
 Data Theory
 Prentice Hall Int Englewood Cliffs NJ 1991 QA76.9.D3 CR9206-0367
 =theory logic incomprehensible
.Close

JuristoMorenoLopez00
.Open JuristoMorenoLopez00
 Natalia Juristo & Ana Maria Moreno & Marta Lopez
 How to Use Linguistic Instruments for Object-Oriented Analysis
 IEEE Software Magazine V17n3(May/Jun 2000)pp80-89
 =DEMO METHOD OOA/D LANGUAGES BNF OMT
 step by step way to map requirements via objectmodel (OM) plus behavior model (BM) to OO? design
 Starts with informal requirements, but notes errors occur in them.
 Splits into static  vs dynamic. Translates into 1:special language; 2: OMT+martin
 missing(p85) : using normalization to assign attributes to class.
 missing(pp88-89) :ref to NIAM?
 wrong(p87) : when a method operates on all the classes in a sub-hierarchy "the method will belong to the highest class".  leads to anomolous classes with no behaviors plus highlevel classes with complex logic and so reduced maintainabillty.
.See [BottingJuristo00]
.Close

Kahn92
.Open Kahn92
 Ken Kahn
 A Braid of Research Threads(in The Fifth Generation Project)
 Comm ACM V36n3(Mar 1993)pp77-82
 =EXPERIENCE OBJECT-ORIENTED GRAPHIC DESIGN
.Box
p79-80
"Saraswat and I began work on a visual syntax for concurrent logic
programs.  he Syntax was based on the topology of drawings.  It was
designed so that it was well suited not just for program sources but also
as a basis for generating animations of program executions.  One discovery
was that object-oriented programs did not come out so clumsy and verbose
when they where drawn instead of typed. "
.Close.Box
.Close

KalishMontague64
.Open KalishMontague64
 Donald Kalish & Richard Montague
 Logic: Techniques of formal reasoning
 Harcourt Brace & World Inc. NY NY 1964
 =TEXT LOGIC
 Natural deduction with boxes withn boxes.
 Brilliant.
.Close

Katz90
.Open Katz90
 Robert L Katz
 Business/Enterprise Modeling
 IBM Systems Journal V29n4(1990)pp509-525
 =ADVERT MODEL DATA PROCESS
.Box
 p510..511(Figures 1 &2) modeling across the life cycle(data,process, network)><scope, ERD,Logical, technology=design, detailed=implemented)

.Close.Box
.Close

KauffmannMoore97
.Open KauffmannMoore97
 Matt Kaufmann & J S Moore
 An Industrial Strength Theorem Prover for a Logic Based on Common LISP
 IEEE Trans Softw Eng VSE23n4(Apr 1997)pp204-213
.See http://www.cli.com/
 =EXPERIENCES PROOF LOGIC LISP ACL2 hardware CLI Nqthm
.Close

Kaye07
.Open Kaye07
 Richard W Kay
 The Mathematics of logic: a guide to completeness theorems and the applications
 Cambridge UP NY NY 2007 ISBN 052170877X $CR 0902-0126
 =UNREAD THEORY LOGIC MATHEMATICS SEMANTICS Zorn AC Posets TARSKI  P=NP 
.Close

KazmanChen90
.Open KazmanChen90
 Rick Kazman & Hong-Mei Chen
 the metropolis model -- a new logic for development of crowdsourced systems
 Commun ACM V52n7(Jul 2009)pp76-84
.See http://doi.acm.org/10.1145/1538788.1538808
 =ESSAY WEB/NET COMMONS F/OSS ONION SERVICES CROWDSOURCE JAD CBSS LIFECYCLE ANALYST DESIGN ECONOMICS ITERATION. DISTRIBUTED EVOLUTION PEOPLE COMMONS
 CBSS::="community-based service systems", following
.Net
 not producing goods for consumption. Not centralized.
 open teams.  
 Mashability -- reuse.
 conflicting, unknowable requirements -- discover by doing, emergent.  
Continuous evolution. 
 Focus on operations. Start with a working system and aim for no downtime. 
 Sufficient correctness. Perpetual Beta.  
 Unstable resources -- many parallel prosumers. 
prosumer::= produce & consumer.
 Emergent behavior. Nondeterministic. 
.Close.Net
 metropolis_model::onion=kernel+periphery+masses. 
 principles:
.Box
 crowd management>project management. 
 promotion through ranks, attracting developers, meritocracy. 
 split kernel services from peripheral services. 
 pernipheral work is done by crowdsourcing, kernel by higher ranked developers. 
 ubiquitous operations even as it evolves. 
.Close.Box
 implications: no phases, align business to crowd, not control but lead, tutorials and examples, usability.  Requirements come from the periphery, forums help but can be shortcircuited. Architecture vital core. Small modular kernel. Tools for Testing, bug reporting and tracking. Flexible delivery. High availability.  
.Close

KennedyEberhart02
.Open KennedyEberhart02
 James Kennedy & Russell C Eberhart
 Swarm Intelligence
 Morgan Kaufman 2001 ISBN 1-55860-595-5 QA337.3 K45
 =IDEA NON-ALGORITHMIC NONSEQUENTIAL OPTIMIZATION
 In a swarm individuals tend to both move toward their topological neighbors, but also toward the individual that seems to be doing best.
 Claims to be useful and effective.
 Overgeneralized (?) to argue that intelligence is dependant on the interaction of individuals.
 Useful survey of many years of experiments with systems made of interacting individuals.
.Close

Khanna91
.Open Khanna91
 S Khanna
 Logic Programming for Software Verification and testing
 Comput Jnl V34n4(Aug 1991)pp350-357.
 =DEMO LOGIC V&V TESTING
.Close

Kiniry02
.Open Kiniry02
 Joseph R. Kiniry <kiniry@acm.org>
 Semantic Component Composition
 Submitted to GCSE/SAIG '02, arXiv.org e-Print archive Mon, 15 Apr 2002
.See http://www.arxiv.org/abs/cs.SE/0204036and Ph.D. Thesis CalTech.
 =ADVERT THEORY MODULES CORRECTNESS CONTRACT REUSE COMPONENTS SEMANTICS Kind-theory LOGIC QUALITIES BON Jiki
 author attempted to develop a way to describe components, calculate inter-operation, and to lead automatically generating adapters to connect components.
 `instance : kind`
  kinds: 2  inheritance relations, 2 inclusion relations, several equivalences, 2 realization relations, 3 composition operators, 2 interpreter mappings, a canonical operator [_]
 Compare with many previous logistic systems going back to Aristotle.
 semantic_ properties:=meta_information | dependencies | inheritance | contractual | concurrency | usage | pending_work | versioning | documentation | Miscellaneous.
 meta_information:= author | bon | bug | copyright | description | history | license  |  title, 
 dependencies:= references  |  use.
 inheritance:= hides  |  overrides  |  realizes,
 contractual:=ensure  |  generate  |  invariant  |  modifies  |  require,
 usage:= param  |  return  |  exception.
 pending_work:= idea  |  review  |  todo.
 versioning:= version  |  deprecated   |  since.
 documentation:= design  |  equivalent  |  example  |  see.
 Miscellaneous:= guard  |  values  |  time_complexity   |  space_complexity.
.Close

Kleinberg08
.Open Kleinberg08
 Jon Kleinberg 
 The Convergence of Social and Technological networks 
 Commun ACM V51n11(Nov 2008)pp66-72
.See http://doi.acm.org/10.1145/1400214.1400232
 =EMPIRICAL 6DEGREES SMALL WORLDS GRAPHS WEB/NET Milgram  SOCIOLOGY CONTAGION MIMETICS IDEAS
 Evidence that real social networks are "small worlds" as predicted.
 Evidence that ideas spread in jagged trees through the network.
 "Contagion as a Design Priciple" 
.Close

KoMyersCoblenzAung06
.Open KoMyersCoblenzAung06
 Andrew J Ko & Brad Myers & Micheal J Coblenz & Htet Htet Aung 
 An Exploratory Study of How Developers Seek, Relate, and Collect Relevant Information during Software Maintenance Tasks
 ICSE'05 & IEEE Computer Magazine  V39n12(Dec 2006)pp971-987  
 =EXPERIMENT SIMULATED MAINTENANCE INTERUPTIONS TECHNICAL Eclipse Java Swing Paint
 Information_Foraging::=the BIBLIOGRAPHY(authors=>"P Pirolli &S K Card", title=>"Information Foraging", citation=>"Psychological Review V106n4 (1999)pp643-675").
 Took video records of developers modifying and correcting bugs in apaint program.
  Coded the actions into 9 types: Handling information(15%), reading code(12%), editing code, navigating dependencies, searching for names, testing, reading Java API, switching applications,reading task description(2%).
 Early perceptions of bugs can lead to wasted time exploring irrelevant code.
 Enhancements: developers had to search for a place to extend the existing framework and for examples to copy and modify.
 Developers used "Find" dialog, Eclipse's multiple windows,   What is relevant?
When interupted developers always complete there current editting task before acknowledging the interuption, but sometimes forgot to save the edited file!
 Three states: Search; Relate; Collect.
 Need better ways to search for relevant code.  Good names are vital! Perhaps use hovering to show header info on methods fro example.
 Need less overhead in navigating and viewing code. EG highlight code to show dependencies of nearby code rather than menus.
 Show many fragments of code in separate subwindows?
 See
.See [KoMyers10]
.Close

Kobryn02
.Open Kobryn02
 Chris Kobryn
 Will UML  2.0 Be Agile or Awkward
 Commun ACM V45n1(Jan 2002)pp107-110
 =HISTORY UML 1.* =ESSAY on UML 2.0
 Second system effect: 
.See [Brooks95]
 UML2.0 will have 4 parts: infrastructure, superstructure, OCL, and Diagram Interchange
 Resources
.See http://www.omg.org/uml
.See http://www.uml-forum.com/
.See http://www.telelogic.com/publications/uml_models/
.Close

Kowalski79
.Open Kowalski79
 Robert Kowalski
 Algorithm=Logic+Control
 Commun ACM V22n7(Jul 1979)pp424-436
 =DEMO logic-programming non-sequential prolog optimization
.Close

Kowalski79b
.Open Kowalski79b
 Robert Kowalski
 Logic for Problem solving
 Elsevier Science NY NY 1979 1983 ISBN 0-444-00365-7 QA76.K68
 =TEXT LOGIC FORMAL PROLOG THINKING
.Close

Krakovsky11
.Open Krakovsky11
 Marina Krakovsky
 Deus Ex Machina 
 Commun ACM V54n5(May 2011)p22 
.See http://doi.acm.org/10.1145/1941487.1941496
 =ARTICLE PROOF ONTOLOGICAL EXISTENCE GOD PROVER9 LOGIC PROVER9
 Authors Paul Oppenheimer and Edward Zalta: "A Computationally-Discovered Simplification of the Ontological Argument". Australasian Journal of Philosophy 89 (2): 333-349. 2011.
 Details 
.See http://mally.stanford.edu/cm/ontological-argument/
 More at
.See http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.151.7483&rep=rep&type=pdf
(PDF).
.Close

KrishnamurthiFisler07
.Open KrishnamurthiFisler07
 Shriram Krishnamurthi & Kathi Fisler
 Foundations of Incremental Aspect model-checking
 ACM TOSEM Trans Software Eng & Methodology V16n2(Apr 2007)pp1-39
 =THEORY ASPECT MODULES EVOLUTION FSM CTL MODAL LOGIC
 Models code as finite state machines with special (paired) transitions for
entering and leaving subprograms.
 Aspects are modeled as finite state machines that are place in
before/after/arround the special transitions.
 Aspects placed using regular expression on the state of the stack of calls.
 CTL modal operators used to state required properties.
.Close

Krug00
.Open Krug00
 Steve Krug
 Don't Make me Think: A Common sense approach to web usability
 New Riders 2000 TK5105.888 K78 ISBN 0-7897-2310-7 
 =GUIDE USER HCI WWW/NET PEOPLE TEAMS
 "Advanced Common Sense"
 `Expert usability review` != `usability testing`
 (1) self evident | (2) self explanatory
  Users scan pages, they don't read them. We guess.  We muddle through.
   Visual hierarchy and logic.  Conventions.  Break up into areas.  Make clickabilty obvious.  Minimize noise.
  Omit words! Instructions and happy talk.
  ask(search) or browse?
  navigation info: site id, utilities( a way home, a way to search,...), contents(with drop down secondary navigation)
  Page names on all pages, and match link text that refs them.
  bread crumbs: You are here X>Y>Z>...
  Tab dividers. Drawn right and front tab clearly in front.
  home pages: all the above + tag line + ...+where to start
 design team problems: wars of religion -> resolve by testing the particular case 
  How to do usability tests.....
.Close

Kruchten95
.Open Kruchten95
 Phillipe B Kruchten(Rational Software pjruchten@rational.com)
 The 4+1 View Model of Architecture
 IEEE Software Magazine(Nov 1995)pp42-50
 =ADVERT SCENARIOS METHOD
 logical+process+physical+development centered on Scenarios
 each view uses Elements+forms+rationale/constraints
.Close

Kruchten08
.Open Kruchten08
 Philipe Kruchten 
 The Biological Half-life of Software Engineering Ideas
 IEEE Software Magazine V25n5(Sep/Oct 2008)pp10-11 
 =SURVEY IDEAS 1988..2008
 Half_life(C)::=`The time taken before 50% of a chemical C is removed from a body`, example: Half_life(caffeine) =~= 3.5.hrs.
 Out of 50 items in IEEE Software from 1988 no more than 3 are still important.
 This implies a Half_life of about 5.years.
 Professional organizations enforce continuing professional development.
 More important to learn how to learn than learn the language/system of the day.
 (dick)|- Compare the half life used to model radioactive decay.
 (dick)|- Suggests exponential decay:
	  amount (t) = amount (t0) * 2 ** ((t0-t)/ half_life) ).
 (dick)|- `Which ideas are strong enough to survive?`
.Close

Kung89
.Open Kung89
 C H Kung
 Conceptual Modeling in the Context of Software Development
 IEEE Trans Soft Eng vSE-15 n10(Oct 1989)pp1176-1187
 =DEMO data ERD DFDs logic Petrie nets System
.Close

KuperVardi93
.Open KuperVardi93
 Gabriel M Kuper & Moshe Y Vardi
 The Logical Data Model (LDM)
 ACM Trans Database Syst v18n3(Sep 1993)pp379-413 CR9407-0472
 =THEORY DATA

theory for LDM

OO data model that generalizes the relational hierarchical and network

review of 7 other attempts

none provide both conceptual data and a well defined retrieval mechanism/query language

defines a DB schema as a digraph. leaves are dta, internal nodes are connections from objects with separate names and values.

sect 2 intro, sectn 3 math defs, sectn 4 logic og LDM, sectn 5 & 6 query languages

Strong theoretical foundation for future DBMSs
.Close

Kurki-Suonio94
.Open Kurki-Suonio94
 Reino Kurki-Suonio<rks@cs.tut.fi>
 Real-Time: Further Misconceptions (or Half-Truths)
 IEEE Computer Magazine V27n6(Jun 1994)pp71-76
 =ESSAY REAL TIME
.Box
confusion of theoretical model with coded programs.. problems defining real-time systems... possibility of fairness allowing the logical specification of deadlines.
.Close.Box
.Close

KwonAgha11
.Open KwonAgha11
 YoungMin Kwon & Gul Agha
 Verifying the evolution of probability distributions governed by a DTMC
 IEEE Trans Software Engineering  V37n1(Jan/Fed 2011)pp126-141 
 =THEORY DEMO TOOL MODAL LOGIC MODEL CHECKING iLTL MARKOV DISCRETE TIME BUCHI 
 Model has both probabilities and qualities on transitions and so expected value on paths. Probabillitues and qualities used to give modes in the logic.
.Close

LafontaneLedruSchobbens91
.Open LafontaneLedruSchobbens91
 Christine Lafontane & Yves Ledru & Pierre-Yves Schobbens
 An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM case Study
 Commun ACM V45n5(May 1991)pp62-ff
 =EXPERIMENT FORMAL VDM LOGIC
 Review: CR 9204-0229
.Close

Lakatos76
.Open Lakatos76
 Imre Lakatos (edited by John Worral and Elie Zahar)
 Proofs and Refutations
 Cambridge University Press 1976
 =PHILOSOPHY MATHEMATICS PROOFS SOCIAL PROCESS
 Describes an advanced seminar in mathematics where the students duplicate 
the key points in the history of a particularly elegant theorem in the 
theory of polyhedra.
 He makes it clear that proofs are often refuted. Mathematics grows by a 
process of proof, refutation, and reproof. 
 The exception improves the rule more often than not.
 The author wanted to decrease the dogmatism of mathematics, and in 
particular the dogma that mathematical knowledge grows by deducing truth 
from known truths.
 He shows that actual mathematics develops in an illogical fashion because 
it grows by discovering the underlying assumptions as well as by working 
from these to prove conclusions.
 The end result of years of exploration is an axiomatic structure like
Euclid.  But this structure is not how the field developed.
 Lakatos tabulates specific ways of tackling facts that don't fit the
theorem and its (putative) proof.
 See
.See [DeMilloLiptonPerlis79]
.Close

Lamport90a
.Open Lamport90a
 Leslie Lamport
 A Temporal Logic of Actions(TLA)
 Report 57 from Systems Research Center Digital Equipment Corpn(1st Apr 1990) &  Revised as Lamport91
 =MATHEMATICAL non-sequential formal dynamic  modal logic
.Close

Lamport91
.Open Lamport91
 Leslie Lamport
 The Temporal Logic of Actions(TLA)
 Report 79 from Systems Research Center Digital Equipment Corpn(25th Dec 1991)
 =MATHEMATICAL non-sequential formal dynamic  modal logic
 Revision of Lamport90b
.Close

Lamport94a
.Open Lamport94a
 Leslie Lamport
 Processes are in the Eye of the Beholder
 Report #132 from Systems Research Center Digital Equipment Corpn(25th Dec 1994)
 =THEORY NONSEQUENTIAL LOGIC
.Box
(abstract)
A two-process algorithm is shown to be equivalent to an N-process
one, illustrating the insubstantiality of processes.  A completely
formal equivalence proof in TLA (the Temporal Logic of Actions) is
sketched.
.See http://www.research.digital.com/SRC/publications/src-rr.html
.Close.Box
.Close

Lamport94b
.Open Lamport94b
 Leslie Lamport
 Unknown
 ACM TOPLAS (May 1994)pp872-923
 =MATHEMATICAL non-sequential formal dynamic  modal logic
 Cannonical version of 
.See [Lamport91]
 TLA Temporal Logic of Actions.
.Close

Lamport94c
.Open Lamport94c
 Leslie Lamport
 Writing Proofs
 Microsoft Research
.See http://research.microsoft.com/en-us/um/people/lamport/proofs/proofs.html
 =IDEA PROOFS FORMULAS STRUCTURED FORMAL LOGIC MATHEMATICS
 Published off line as
.See [Lamport95]
below.
.Close

Lamport95
.Open Lamport95
 Leslie Lamport<lamport@src.dec.com>
 How to Write a Proof
 American Math Monthly V102n7(Aug-Sep 1995)pp600-608
 =DEMO PROOFS FORMAL LOGIC
.Box
Hierarchically structured proofs in outline style see Abadi & Lamports work.

Q.E.D. is a step representing what needs to be proved:

.As_is Theorem <statement>
.As_is PROOF SKETCH: <english style proof scetch>
.As_is ASSUME: <label>. <predicate> ...
.As_is PROVE: <predicate>
.As_is NumberedList( <number>. <step|predicate> )
.As_is   <number>. Q.E.D.

.As_is LET: <definitions>
.As_is Choose .... such that....

.As_is CASE: statement of assumption
is short for
.As_is ASSUME: Statemnt of assumption
.As_is PROVE: Q.E.D.
.Close.Box
 Also see online reports
.See [Lamport94c]

.Close

Lamport95a
.Open Lamport95a
 Leslie Lamport
 TLA in Pictures
 IEEE Trans SE VSE-21n9(Sep 1995)pp768-775
 =THEORY TLA Formal Graphics temporal logic of actions
.Box
Claims: first use of diagrams to provide complementary multiple formal views.  an aid to presenttion and proof.

Like FSA(states=>predicates, transactions => actions)
out(n):edges out of n, 
d(e) :nodes=destination of edge e,
P(n) :=predicate on node n, 
P'(n) :=primed predicate...
disjoint_predicate:=for all nodes n1,n2(not(P(n1) and P(n2)).

A(n) :=for some e:out(n)(action(n) and P'(d(e)))
two possible formula for meaning of transitions:
 \Delta:=for all nodes n, always(if P(n) then A(n) )
or
 \Delta_bar:=always(some nodes n(P(n) and A(n))).
()|- if \Delta then \Delta_bar
()|- if disjoint_predicates then (\Delta iff \Delta_bar)
.Close.Box
.Close

LamsweerdeDarimontLetier98
.Open LamsweerdeDarimontLetier98
 Axel van Lamsweerde & Robert Darimont & Emmanuel Letier
 Managing Conflicts in Goal-Driven Requirements Engineering
 IEEE Trans SE V24n11(Nov 1998)pp908-926
 =THEORY PURPOSE KAOS LIGHTWEIGHT FORMAL temporal LOGIC views Some EXPERIENCE
 find scenarios leading to divergences. Obstacles are scenarios that make it impossible to meet all the requirements
.Close

LamsweerdeLetier00
.Open LamsweerdeLetier00
 Axel van Lamsweerde & Emmanuel Letier
 Handling Obstacles in Goal-Oriented Requirements Engineering
 IEEE Trans Software Engineering  V26n9(Sep 2000)pp978-1005
 =CASESTUDY  REQUIREMENTS REFINEMENT EXCEPTIONS TEMPORAL LOGIC KAOS
 Requirements can assume too much  reliability in parts of system.
 Should calculate things that can go wrong and allow for them in their requirements.
 p983: "an obstacle defines a set of undesirable behavior; a negative scenario produces a behavior in this set". Obstacles imply a goal is not met but obstacles  must not be inconsistent with the domain - exists a scenario
 Goals have form "at all times...." but obstacles have form : "at some time...."
.See [KjaerMadsen95]
 `user anti-story`!
.Close

LamsweerdeWillemet98
.Open LamsweerdeWillemet98
 Axel van Lamsweered & Laurent Willemet
 Inferring Declarative Requirements Specifications from Operational Scenarios
 IEEE Trans SE V24n12(Dec 1998)pp1089-1114
 =DEMO USER to PURPOSE TLA FORMAL LOGIC LANGUAGE KAOS WHY+WHO+WHEN+WHAT Lift
 Stakeholders may have problems expresssing requirements in abstract but typical scenarios are easier to elicit.
 SCENARIO as example of or counter-example to abstraction
 Scenario=sequence diagram, Goal.types={achieve, Cease, maintain, avoid}.
.Close

LangeChaudronMuskens06
.Open LangeChaudronMuskens06
 Christian F J Lange & Michel R V Chaudron & Johan Muskens 
 In Practice: UML Software Architecture & Design Description
 IEEE Software Magazine V23n2(Mar/Apr 2006)pp40-46
 =POLL 80 Architects +14 CASE STUDIES UML QUANTITY QUALITY METRICS 
 80% used usecase & logical, 50% component & scenarios, 17% deployment.
 Loose adherence to standard.
 Survey presumed a "waterfall" process.
 Problems mentioned in poll. scattered information, incompleteness, disproportion, inconsistency, diagram quality, informality, no conventions. 
 40%+ plan to use more UML metrics.
 Defects in case studies: classes do not fit sequence diagrams, classes with no methods.
 Experiment: most students & practitioners can't detect mismatches between class and sequence diagrams.
 See "Effects of defects in UML models"  in ICSE06 by  Lange & Chaudron.
.Close

LanoGoldsackSanchez99
.Open LanoGoldsackSanchez99
 Kevin Lano & Stephen Goldsack & arturo Sanchez
 specification of a Chemical Process Controller in B
 In 
.See [HincheyBowen99]
pp53-80
 =EXPERIENCE  fORMAL SPECIFICATION REACTIVE  VALIDATION V&V B PCT FSM TEMPORAL LOGIC StateCharts TOOLS
 Chemical process control synthesis.
 Worked but would have liked to have temporal logic to specify dynamics
.Close

LemosSauudAnderson92
.Open LemosSauudAnderson92
 R de Lemos & A Sauud & T Anderson
 A Train Set as a Case Study for the Requirements Analysis of Safety Critical Systems
 Computer Journal V35n1(Feb 1992)pp30-40 CR9307-0516
 =CASE-STUDY REQUIREMENTS Reality
.Box
Faults in Requirements cause disasters

Separate the mission from safety requirements

distinguish Physical  Reality from  System

Use logic for R and Petrie Nets for System.

Timed History Logic
.Close.Box
.Close

Lenat95
.Open Lenat95
 Douglas B. Lenat(mailto:Lenat@MCC.COM & doug@cyc.com)
 CYC: A Large-scale Investment in Knowledge Infrastructure
 Commun ACM V38n11(Nov 1995)pp33-38 +pp45-48(critiques)
 =EXPERIENCE CYC LOGIC ONTOLOGY 
.Close

Lenatetal90
.Open Lenatetal90
 Douglas B. Lenat & R.V. Guha & Karen Pittman & Dexter Pratt & Mary Shephard
 Cyc: Toward Programs with Common Sense
 Commun ACM V233n6(Aug 1990)pp30-49
 =EXPERIENCE CYC LOGIC ONTOLOGY 
.Close

LetierLamsweerde02
.Open LetierLamsweerde02
 Emmanuel Letier & Axel van Lamsweerde 
 deriving Operational Software specifications from System Goals
 SIGSOFT 2002/FSE 10 & ACM SIGSOFT Software Engineering Notes V27n6(Nov 2002)pp119-128
 =DEMO SYSTEM REQUIREMENTS GOAL REFINEMENT PATTERNS LOGIC AND/OR TEMPORAL RT-LTL REALITY ENTITY RELATIONSHIP OPERATION SPECIFICATION
 An operation is a temporal proposition defined by the current truth of a set of preconditions and the truth in the next step of a set of postconditions.
 goal_patterns::=achieve | maintain_avoid.
 achieve::= unbounded_achieve | bounded_achieve | immediate_achieve.
 unbounded_achieve: for always if C then sometime T.
 maintain_avoid::= state_invariance | transition_invariance.
 state_invariance::=global_invariance | after_invariance | in-between_invariance.
.Close

Lev-AmiEtal00
.Open Lev-AmiEtal00
 Tal Lev-Ami & Thomas Reps & Mooly Sagiv & Reinhard Wilhelm
 Putting Static Analysis to Work for Verification: A Case Study
 Proc ISSTA 00 & ACM SIGSOFT Software Engineering Notes V25n5(Sep 2000)pp26-38
 =DEMO TOOL PROOF POINTERS 3-valued  LOGIC GRAPH
.Close

LewisT94d
.Open LewisT94d
 Ted G Lewis(<lewis@cs.nps.navy.mil>Naval Postgraduate School)
 The Next 10000[2] Years: Part II
 IEEE Computer Magazine V29N5(May 1996)pp78-86
 =ESSAY predictions DESIGN REUSE
.Box
Note 10000[2]years = 16.years,

Continues 
.See [LewisT94c]
 networks will survive.

Software as Steam for the future.

Quotes Capers Jones on programmer productivity increasing 3-5% per year ($/fp).

Shows comparison of power of languages.

reates an oportunity for new ideas etc.

Predicts large MIS will go for visual tools and object tools rather than languages.
(compare Keuffel96? - the bubble sort effect).
OT as a stepping stone, discarding functional decomposition and hiding if-then-else logic.
 Errors of inheritance and polymorphism.

 Things lacking and possible fixes:
.Box
 Requirements: continuous adaption
 defects: correct-by-construction
 Avoid big systems, make pieces
 Time: paint programs
 Cost: throwaway parts
 expertise: use tools with artistic skills needed
.Close.Box
 Frameworks with API, Components produced by experts.
 Applets as event handlers with user in control using frameworks and components
.Close.Box
.Close

Li91
.Open Li91
 Xiaofeng Li
 What's so Bad about Rule-Based Programming
 IEEE Software V8n5(Sept 1991)pp103-105
 =DEMO LOGIC PROGRAMMING AI  Technical Maintenance Reliability
.Close

LichtensteinPnueli00
.Open LichtensteinPnueli00
 Orna Lichtenstein and Amir Pnueli
 Propositional Temporal Logics: Decidability and Completeness
 Logic Journal of the IGPL V8n1(Jan 2000)pp55-85
.See http://www3.oup.co.uk/igpl/Volume_08/Issue_01/#Lichtenstein
 =THEORY FORMAL LOGIC TIME PTL
 =HISTORY 20 years
 axioms etc complete and sound relative model, decision procedure using semantic tableau.
 time with a beginning. Basic modal operators: Next, Until, Weak_previous, Since. Defines half-a-dozen others.
.See http://csci.csusb.edu/dick/maths/logic_9_Modalities.html#PTL
.Close

Lifschitz95
.Open Lifschitz95
 Vladimir Lifschitz
 The Logic of Common Sense
 ACM Computer Surveys V27n3(Sep 1995)pp343-345
 =SURVEY AI Logic defaults inertia
.Box
Quotes and refers to Leibnitz's "An Introduction to a secret Encyclopedia": "Everything is presumed to remain in the state in which it is"

The commonsense law of inertia
.Close.Box
.Close

LocascioDarpel93
.Open LocascioDarpel93
 Capt Charles J Locascio & 2Lt Mathew M darpel
 Software Reengineering for the Future with Ada
 IEEE Computer Society Reverse Engineering Newsletter n5&6(Dec 1993)pp4-5
 =EXPERIENCE LEGACY COBOL JCL RENGINEERING Ada DFD REQUIREMENTS
.Box
Replacing13 year-old undocumented suite of COBOL programs and JCL
Into Ada
Analysis of JCL+COBOL, JCL->physical DFD->Logical DFD = 4 diagrams!
cf results with Requirements-> missing, extra, obsolete
preliminary oo design: real world objects
  Prelimnary Object Encyclopedia"
 OOD
 Advanced CASE Technology
 Design Based Maintenance(DBM) : Design+Code is one thing.
 Teamwork DSE(Design sensitive Editor)
 Ada Structure Graphs(ASGs)
 reuse: Booch components, 100s of generic packages, domain library

Ada Helped.
.Close.Box
.Close

Long78
.Open Long78
 Chris Long
 Logical
 =LETTER ENGLISH LOGIC  ITL UNIVERSAL LANGUAGES
 Computer Weekly (UK) (Mar 16 1978)p20
 You can write English logically!
.Close

Lover08
.Open Lover08
  Robert Lover
  Elementary Logic: for software Development
  Springer Publishing NY NY (2008) ISBN 1848000812 $CR 1002-0125
  =UNREAD =TEXT LOGIC
  Notes
.Hole Lover08
.Close

LupuSloman99
.Open LupuSloman99
 Emil C Lupu & Morris Sloman
 Conflicts in Policy-Based Distributed Systems Management
 IEEE Trans Software Engineering V25n6(Nov/Dec 1999)pp82-867
 =THEORY TOOL SYSADMIN MODAL LOGIC
 distinguishes policies that permit actions(A+), forbid actions(A-), require actions(O+ on event), require non-action(O-), O:=Obligation, A:=Authorisation.
.Close

MacLennan79
.Open MacLennan79
 B. J. MacLennan
 Observations on the Differences Between Formulas and Sentences and their Application to Programming Language Design
 SIGPLAN V14n7 (Jul 1979)p51-61
 =DEMO logic languages graphic
.Close

Maddux96
.Open Maddux96
 Roger D Maddux
 Relation-algebraic semantics
 Theor Comp Sci V160n1-2(Jun 1996)pp1-85
 =SURVEY LOGIC SEMANTICS REGULAR-EXPRESSIONS
 meaning of a statement is two elements in a relation algebra.  One element defines what happens if the  statement terminates and the other defines the states when the statement will not terminate.  cf 
.See [Hoareetal87]
.Close

Maiden08a
.Open Maiden08a
 Neil Maiden 
 Requirements 25 years on 
 IEEE Software Magazine V25n6(Nov/Dec 2008)pp26-28
 =HISTORY 1983-2008 REQUIREMENTS 
 14 references
 1970s: Requirements were monolithic and used natural language with "noise, silence, contradiction, ambiguity, and wishful thinking".  VDM
.See [Bekic70]
and JSP
.See [Jackson75]
 available but not used. Pencil and Paper 
 1977: Ross
.See [Ross77]
developed SADT notation (IDEF) and method
.See [Ross85] and story telling.
 1978: 
.See [Jackson78]
System maintains a model of reality.  Leads to JSD in the 1980s 
 1979: DeMarco
.See [DeMarco79]
, Gane&Sarson
.See [GaneSarson79]
, Yourdon
.See [Yourdon75]
& Constantine. DFDs. Logical vs Physical. STDs. Functional decomposition. Informal diagrams.
structured analysis and design.  First CASE tools help draw informal graphics.
 1980s: Greenspan. 
.See [BorgidaGreenspanMylopoulos85]
.See [BorgidaGreenspanMylopoulos94]
Semantic networks, logic, frames model knowledge about situation. RML: the model is collection of objects of different types. Ontology: entities, activities, assertions.  Leads to TROPOS, i*, KAOS (Knowledge Acquisition in Automated Specification).  Goals and Constraints.
Expert systems. 
 1980s: Stakeholders have difficulties articulating requirements. So, repertory grids, card sorting, Laddering.
.See [Maiden09]
 1990s: Ethnography, HCI. Complexity of the working environment. 
 1998: Beyer & Holtzblatt
.See [BeyerHoltzblatt94]
.See [BeyerHoltzblatt95]
: Contextual enquiry. 
 1999: Vicente: Cognitive work Analysis
 2004: 
.See [MaidenGizikisRobertson04]
: Inventing requirements.
 Today: better at identifying stakeholders, use cases and scenarios, quality requirements, reasoning about natural language, multiply viewpoints, detecting and handling conflicts, social techniques, Tracing requirements, tailoring to different domains, training analysts.
 Meanwhile: We are tackling larger and more complex systems.
 Also see
.See [Maiden05]
on requirements research.
.Close

MaidenGizikisRobertson04
.Open MaidenGizikisRobertson04
 Neil Maiden & Alexis Gizikis & Suzanne Robertson
 Provoking Creativity: Imagine what your Requirements Could Be Like
 IEEE Software Magazine V21n5(Sep /Oct 2004)pp68-75
 =EXPERIENCE  REQUIREMENTS WORKSHOP CREATIVITY CORA RESCUE  Pre-USE CASE
 Describes theoretical basis for creative thinking: Diverge; Converge.  Prepare, incubate, illumination, verification.  Cf. CORT TEC Target-Expand-Contract
 RESCUE::="Requirements Engineering with Scenarios for User-centered Engineering".
 CORA::="COnflict Resolution Assistant", for air-traffic Control.  Cf. TCAS projects.
 Used other domains and analogies to explore requirements.  Analogy via a common abstraction.
  Combine random stimuli(eg toy frog) and combinations of requirements.
  Transform problems by relaxing constraints.
  Helps to understand the difficulty of creativity.
  Encourage playfulness.
  Groups and plenary sessions.  Ideas on cards.
  Analogies need a step-by-step guidance.
  It takes time to incubate analogical ideas,
 Structure workshops about ideas rather than creative processes.
  Record the rationale behind ideas.
  Time to let off steam...
  Plan plan and then plan alternatives.
  Need a champion for workshops.
  See Gottesdiener, DeBono, Wickelgreen, ...
.Close

Makinson08
.Open Makinson08
  David Makinson
  Sets, Logic, maths for computing
  Springer NY NY 2008 ISBN 1846288444
  =UNREAD DISCRETE MATHEMATICS
  Notes
.Hole Makinson08
.Close

Malik11
.Open Malik11
  Petra Malik
  A retrospective on CZT 
  Software & Experience 41(2): 179-188, 2011. 
  =EXPERIENCE F/OSS OPEN SOURCE TOOL FORMAL Z Requirements specification verification tools LOGIC Set Theory UNICODE XML Circus
 Community Z Tools on SourceForge. See
.See http://en.wikipedia.org/wiki/Community_Z_Tools
on the Wikipedia.
.Close

MannaPnueli91
.Open MannaPnueli91
 Zohar Manna & Amir Pnueli
 Completing the temporal Picture
 Theor Comput Sci V83n1(Jun 1921)pp97-130 
.See [CR]
9204-0235
 =THEORY LOGIC SPECIFICATION MODAL TEMPORAL ASSERTIONAL
 If a safety, response, or reactivity property can be proved in temporal 
logic then it can be proved in assertional logic
.Close

MannaPnueli92
.Open MannaPnueli92
 Zohar Manna & Amir Pnueli
 The Temporal Logic of Reactive and Concurent Systems: Systems
 Springer Verlag NY NY 199?
 =THEORY MODAL TEMPORAL LOGIC
.Close

MannaWaldinger85
.Open MannaWaldinger85
 Zohar Manna & Richard Waldinger
 The Logical Basis for Computer Programming: Vol 1 Deductive reasoning
 Addison Wesley series in C Sci 1985
 =TEXT logic
.Close

Mankin78
.Open Mankin78
 R Mankin
 Loglan -- a more flexible language
 =LETTER Esperanto vs Loglan Volapuk LOGIC  ITL UNIVERSAL LANGUAGES
 Computer Weekly (UK) (Apr 13 1978)p16
 Argues that an ITL must be artificial so that it does not grow, adapt, and develop dialects!
 Rebuttal: Esperanto is used widely and yet has no dialects.
.Close

Markus83
.Open Markus83
 M Lynne Markus
 Power, Politics, and MIS Implementation
 Commun ACM V26n6(Jun 1983)pp430-444
&
.See [MyersAvisson02]
Chapter 3, pp19-48
 =EXPERIENCE  PEOPLE SYSTEMS RESISTANCE POLITICS ORGANIZATION MANAGEMENT FIS
 In this case People resisted a new system not just because it wasn't good enough, or because they were not trained etc, but because the new Financial Information System was a ploy to change the organization.
 New FIS system tended to move data and power toward a centralized system and away from divisional centers.  Divisions fought the system.
 Sometimes it is better to change the organization first and then change the technological systems in use.
.Close

MassonetLamsweerde97
.Open MassonetLamsweerde97
 Phillipe Massonet & Axel van Lamsweered
 Analogical Reuse of Requirements Frameworks
.See [RE'97]
 =ADVERT KAOS SPECIFICATION LANGUAGE ontology  temporal logic graphic tool
.Close

MathewsMcGee90
.Open MathewsMcGee90
 Robert W Matthews & William C McGee
 Data Modeling for Software Development
 IBM Systems Journal V29n2(1990)pp228-235
 =DEMO Conceptual vs Logical vs Physical
 p233 orthogonal to Zachman
.Close

MattoliniNesi01
.Open MattoliniNesi01
 Riccardo Mattolini & Paolo Nesi
 An Interval Logic for real-Time system Specification
 IEEE Trans Software Engineering  V27n3(Mar 2001)pp208-227
 =THEORY MATHEMATICAL LOGIC TEMPORAL SPECIFICATION LANGUAGE TILCO
.Close

MayhewMGouHaaseHartemink12
.Open MayhewMGouHaaseHartemink12
 Michael B Mayhew & Xin Guo & Steven B Haase & Alexander J Hartemink
 Close encounters of the collaborative kind
 IEEE Computer Magazine V45n3(Mar 2012)pp22-30
 =ARTICLE ANALYSIS DESIGN ITERATION BIOLOGY YEAST DOMAIN LANGUAGE
 Describes a collaborative development of software for modeling a biological process and answering biological questions about it. 
  Illustrates need to find and develop a common language for the stakeholder's domain. 
  Need to answer biological questions. 
In general: make sure you know what the user's want.
Whu not use cases?
  Process was iterative. 
.Close

McCamantErnst03
.Open McCamantErnst03
 Stephen McCamant & Michael D Ernst
 Predicting Problems Caused by component upgrades
 FSE-11 & ESEC 9 & ACM SIGSOFT Software Engineering Notes V28n5(Sep 2003)pp287-296
 =DEMO MODULE TESTING LOGIC CONTRACT V&V EVOLUTION Daikon Simplify PERL
 Before putting an upgraded component into an application, use the application+old component to generate a mathematical contract for the old component, then derive a similar contract for the new one.  Only safe if the new contact is stronger than the old one.
 contracts::=$ Net{ pre, post: @States}.
 For contracts c1, c2, c1 is_stronger_than c2 ::= (c1.pre ==> c2.pre) and ((c1.pre&c2.post)==> c1.post).
 Worked well on to PERL module upgrades!
 Nice example of upgrading swap: will work in a bubble sort, but not in a particular selection sort.
.Close

McCannRoman98
.Open McCannRoman98
 Peter J McCann & Gruia-Catalin Roman
 Compositional Programming Abstrations for Mobile computing
 IEEE Trans Soft Eng V24n2(Feb 1998)pp97-110
 =ADVERT non-sequential Net/Web LANGUAGES(UNITY) LOGIC PROOF
.Close

McCannRoman99
.Open McCannRoman99
 Peter J McCaqnn & Gruia-Catlin Roman
 Modeling Mobile IP in Mobile UNITY
 ACM TOSEM V8n2(Apr 1999)pp115-146
 =CASESTUDY MOBILE UNITY LOGIC PROOF Protocol
 
.See [McCannRoman98]
.Close

McCarthy87
.Open McCarthy87
 John McCarthy
 Generality in Artificial Intelligences
 Commun ACM V30n12(Dec 1987)pp1030-1035 based on 1971 Turing award talk
 =ESSAY AI LOGIC LPC  not PROLOG situation calculus frame problem nonmonotonicity. 
 Similar problems arrise in formal specifications:
.See [Borgidaetal95]
.Close

McClintock97
.Open McClintock97
 Colleen McClintock
 The Logic of Business Rules
 Software Development magazine V5n11(Nov 1997)pp44-48+50
 =DEMO DATA REALITY LOGIC CORBA IDL
 DATA encodes REALITY LOGIC: repository to collect formulate store and 
maintain rules(Rochade/Microsoft/Platinum) hence models diagrams 
executable(CORBA IDL) rule servers
.Close

McRae02
.Open McRae02
 Eric McRae
 Tracking Down Killer Bugs
 Dr. Dobbs #335(Apr 2002)pp58+60-61+63-64
 =EXPERIENCE EMBEDDED DEBUGGING TPU AUTOMOTIVE microcode ashware
 finding an unpredictable hard/software bug close to the deadline in code controlling a motor.
 Test platform for debugging cost $3500 -- real time simulators of environment and system + logic analyzer. +$700 for Linux compatible debugger.
 Bug found by inspiration, data gathering, hardware simulation and monitoring, plus *explaining* the situation in detail.
.Close

Mercurioetal90
.Open Mercurioetal90
 V J Mercurio & B F Meyers & A M Nisbet & G Radin
 AD/Cycle Strategy and Architecture
 IBM Systems Journal V29n2(1990)pp170-188
 =ADVERT METHODS AD/Cycle IBM
.Box
p172-173: model..specs...logic+screens+DB I/O, Build, Install, Maintain

(Software Magazine field report September 1993) |- IBM abandons AD/Cycle as a main frame product.
.Close.Box
.Close

MetayerEtAl11
.Open MetayerEtAl11
 Daniel Le Metayer & Manuel Maarek & Eduardo Mazza & Marie-Laure Potet & Stephane Frience & Valerie Viet Triem Tong & Nicolas Craipeau & Ronan Hardouin
 Liability Issues in Software Engineering: the use of formal methods to reduce legal uncertainties
   Commun ACM V54n4(Apr 2011)pp99-106
.See http://doi.acm.org/10.1145/1924421.1924444
 =DEMO MASS MARKET SOFTWARE CONTRACTS LOGIC TOOLS CHECKING EULA
 Shows how symbolic logic can be used to clarify who is responsible for various bad things happening.
 formal model in terms of mappings `time stamps` ->@( {`Send`, `Receive`} >< (`Components` | `Users` )^2 >< `Data`).
 Example: A document is only received if it has been sent:
	For all documents d ( (`Receive`, `Serv`, `SigApp`, d) in T(\theta) iff (`Send`,  `SigApp`, `IO`, d)  ).
 Liability maps `Claims`><`Traces`><\theta -> @(`Parties`).
.Close

Meyer85
.Open Meyer85
 Bertrand Meyer
 On Formalism in Specification
 IEEE Software V2n1(Jan 1985)pp6-27
 =DEMO formal logic non-sequential PURPOSE Reality
.Box
Examines line breaks problem, notes structure clash and use of pipes and inversion for solution.

inspiration for my 'br' program:
.See http://www/dick/tools/br.d.html

.Close.Box
.Close

Mills75
.Open Mills75
 Harlan D Mills
 The New Math of Computer Programming
 Commun ACM V18n1(Jan 1975)pp43-48
 =THEORY MATH LOGIC structured CLEANROOM
 Also presented paper that year on getting programs right. International Conference on Reliable Software.(Berard)
 Refed in Zelkowitz90, cites
.See [BohmJaccopini66]
.Close

MorrisBunkenburgTyrrell09
.Open MorrisBunkenburgTyrrell09
 JOSEPH M. MORRIS & ALEXANDER BUNKENBURG & MALCOLM TYRRELL
 Term Transformers: A New Approach to State
 ACM Trans. Program. Lang. Syst. V31n4 (May 2009)a16:1-42
.See http://doi.acm.org/10.1145/1516507.1516511
 =IDEA TERM TRANSFORMERS PREDICATE wp LANGUAGES SEMANTICS LOGIC PROOF Lambda axiomatic denotation Dijkstra
 phase ::=command "|>" term.
 In the text \righttriangle is used for my "|>" above.
 Example:
     x:=x+1 |> x^2 = (x+1)^2.
 Uses a lambda calculus based language of commands and terms to establish mathematical `bona vides`.
.Close

MorzentiSanPietro
.Open MorzentiSanPietro
 Angelo Morzenti & Pierluigi San Pietro
 Object-oriented logical specification of time-critical systems
 TOSEM V3n1(Jan 1994)pp56-98 CR9503-0166
 =THEORY OBJECT_ORIENTED LOGIC SPECIFICATION TIMING
.Close

MoserEtal97
.Open MoserEtal97
 L E Mose & Y S Ramakrishna & G Kutty & P M Melliar-Smith & Laura K Dillon
 A Graphical Environment for the Design of Concurrent Real-Time Systems
 ACM TOSEM V6n1(Jan 1997)pp1-30
 =THEORY GRAPHIC LOGIC SPECIFICATION TIMING
 RTGIL::=Real-time Graphical Interval Logic
.Close

MunakataJani94
.Open MunakataJani94
 Toshinori Munakata & Yashvant Jani
 Fuzzy Systems: An Overview
 Comm ACM V37n3(Mar 1994)(AI issue)pp69-76
 =SURVEY =ADVERT FUZZY LOGIC MATHEMATICS
.Close

MyersJP90
.Open MyersJP90
 J. Paul Myers Jr.
 The Central Role of Mathematical Logic in Computer Science
 ACM SIGCSE V22n1(Feb 1990)pp22-26
 =ESSAY logic formal
.Close

Nagel56
.Open Nagel56
 E Nagel
 A Formalization of Functionalism
 Logic Without Metaphysics Free Press 1956 pp247-283, reprinted Emery69
 =ESSAY FUNCTION SYSTEMS PURPOSES
 p298. distinguishes mathematical function from purpose.
 p311.  functional analysis in social systems requires a standardized/patterned/repetitive items
.Close

Naur07
.Open Naur07
 Peter Naur 
 Computing versus Human thinking
 Commun ACM V50n1(Jan 2007)pp85-94 + letter V50n4(Apr 2007)pp7-8  
 =HISTORY REJECTING MODERN  PSYCHOLOGY LOGIC TURING AI vs plastic neural nets  $CR 0801-0095 
 William James
 Science as description not theorizing.
.Close

NaumovichClarke00
.Open NaumovichClarke00
 Gleb Naumovich & Lori A Clarke
 Classifying Properties: An alternative to the Safety-Liveness Classification
 
.See [FSE8]
pp159-168
 =IDEA TEMPORAL LOGIC SPECIFICATION ANALYSIS SAFETY LIVENESS
 classifies properties in terms (1) that describe finite, infinite, or both kinds of sequences events, pus (2) that must be checked on finite, infinite, or both kinds of sequences of events.
.Close

Nicollinetal92
.Open Nicollinetal92
 Xavier Nicollin & Joseph Sifakis & Sergio Yovine
 Compiling Real-Time Specifications into Extended Automata
 IEEE Trans SE-V18 n9 (Sep 1992)pp794-804
 =THEORY timeout watchdog gnerates event driven FSM from logical specification
.Close

NentwichEtAl03
.Open NentwichEtAl03
 Christian Nentwich & Wolfgang Emmerich & Anthony Finckelstein & Ernst Ellmer
 Flexible Consistency Checking
 ACM TOSEM Trans Software Eng & Methodology V12n1(Jan 2003)pp28-63
 =DEMO WEB/NET DOCUMENTATION XML xlinkit webservice LOGIC CONSISTENCY MANAGEMENT DIFFERENCING TOOL UML Java EJB
 Links are not placed in documents. Connect elements in other documents.
 Four kinds of constraint: standard, extension, integration, custom.
 xlinkit::webservice=http://www.xlinkit.com.
.Close

Nishidaetal91
.Open Nishidaetal91
 Fujio Nishida & Shinobu Takamatsu & Yoncharu Fujita & Tadaaki Tani
 Semi-Automatic Program Construction Using Library Modules
 IEEE Trans SE-17 n9 (Sep 1991)pp853-871 CR9302-0087
 =THEORY re-use logic natural PURPOSE MAPS \equiv MATHS
 refinement := unification and proof by refutation of horn clauses of structured specification with problem parts
 library with specifications.
.Close

Nissanke99
.Open Nissanke99
 Nimal Nissanke
 Introductory Logic and Sets for Computer scientists
 Addison Wesley Longman 1999 ISBN 0-201-17957-1 QA76.9 L63N57
 =TEXT Z LOGIC DISCRETE MATH
  for CSUSB csci556/656
.Close

OConnell02
.Open OConnell02
 Laurie O'Connell
 Communications Gap
 Software Development Magazine V10n5(May 2002)pp17
 =REPORT SOFTWARE QUALITY
 Reports on a 10 year DoD "National software quality Experiment" in the "Software Inspection Lab".  No appreciable reduction in errors or improvements in process.
 Main defects noted: 41% lack of traceability, 23% infringing standards. 7% logic errors. 7% functionality. 5% syntax. 5% initial values. 4% maintainability.
 Software products are not "well connected" to their business requirements.
.Close

Okrent09
.Open Okrent09
 Arika Okrent
 In the Land of Invented Languages: Esperanto Rock Stars, Klingon Poets, Loglan Lovers, and the Mad Dreamers Who Tried to Build A Perfect Language
 Random House Publishing Group Pub. Date: May 2009 ISBN-13: 9780385527880 352pp
 =SURVEY =HISTORY 900 ARTIFICIAL LANGUAGES Blissymbolics MATHEMATICS LOGIC Elvish Esperanto Gestuno Wilkins thesaurus Dalgarno Zamenhoff ONTOLOGY
 Repeatedly somebody has had the same ideas for improving on natural
"grown" languages -- using logic, setting up an ontology, using symbols,
using numbers, using european languages, etc.
 There is no natural ontology/symbology/adamic language.
 Humans evolve the language that they use.
Language inventors come into conflict with language users.
 Bliss symbols for disabled children -- students needs vs Bliss's obsessions.
 Loglan vs Lojban.  Brown vs the Loglanists.
 Writing Lojban is like programming.  Speaking it seems to be impossible.
 Learning a new language leads you to see the world differently.
 Benjamin Whorf's Hypothesis?
 Didn't mention e-prime or SLUNT...
 You thoughts can go here:
.Hole
.Close

OrtinEtal04
.Open OrtinEtal04
 Francisco Ortin & Benjamin Lopez &J Baltasar Garcia Perez-Schofield
 Separating Adaptable Persistence Attributes through computational Reflection
 IEEE Software Magazine V21n6(Nov /Dec 2004)pp41-49
 =DEMO TOOL SEPARATE PERSISTENCE DATA vs BUSINESS LOGIC  Nitr0 Java REFLECTION
 Notes
.Close

Owreetal95
.Open Owreetal95
 Sam Owe & John Rushby & Natarajan Shankar & Friedrich von Henke
 Formal Verification for Fault-Tolerant architectures: prolegomena to the Design of PVS
 IEEE Trans on Software Eng VSE-21n2(Feb 1995)pp107-125
 =ESSAY FORMAL LOGIC TOOL partial functions SPECIFICATION
PVS::=http://www.csl.sri.com/pvs.html,
`System for generating proofs`.
.Box
PVS next generation after EHDM(1984)

interactive

uses ASCII input plus map to LaTeX and graphics, under EMACS
ftp://ftp.csl.sri.com/pub/pvs

Application to concurrent faulty systems.

p114: "Most of the proofs ... not to mention many of the theorems and some of the algorithms wer incorrect when we started... our axiomatizations were occassionally unsound, and sometimes they were sound but did not say what we thought they did... our verifiactions are seldom finished: changed assumptions and requirements, the desire to improve an argument or a bound, and simple experiementation, have led us to revise some or all of our verifiactions several times... [they are used] by someone other than their original developer.....structured....modular"

"we found that substantial effort was expended on the formal development of 'background theories' such as summations, bitvectors, finite sets, and so on.  Clearly, it is necessary that such theories should be made available in libraries for future reuse."

Help in debugging specifications.

working(r):set[R]={r | member(c, OK(r))}.

p118: "Some specification environments allow specifications to be expressed directly in terms of mathematical symbols[...]we have found that the burden of supporting these conveniences outway the benefits, bringing in the wake such menaces to productivity as structure editors, and a plethora of mouse and menu selections.  In the US, at least, most scientists and engineers are fast touch typists, and we ind a conventional program editor provides a more productive environment for rapid interaction than a graphical user interface[...]LaTeX,...graphical representation of module dependencies and proof trees...hypertext"
.Close.Box
.Close

PahlCasey03
.Open PahlCasey03
 C Pahl & M Casey
 Ontology support for web service processes
 FSE-11 & ESEC 9 & ACM SIGSOFT Software Engineering Notes V28n5(Sep 2003)pp208-216
 =FORMAL WEB/NET LOGIC ALGEBRA LTS Kripke temporal description LANGUAGES
 Many definitions, no results.
.Close

Pappas92
.Open Pappas92
 T.L.(Frank) Pappas
 Logical Document Design with Scientific Word
 IEEE Computer V25 n8(Aug 1992)p85
 =Review TOOL WRITING MATHEMATICS LOOK_AND_FELL vs SEMANTIC STRUCTURE TAG
 Chapter 3: lexical and output formatting.
.Box
Quote
"When writing a paper, you should only be concerned with such issues as identifying section headings, stating theorems, providing bibliographic citations, and making reference to other potions of the paper.  These have nothing to do with the papers appearance, which varies with the style used by the journal it will appear in."
"tags" marker: <id> <-----< ref: <id>
.Close.Box
.Close

Parnas77
.Open Parnas77
 David Lorge Parnas
 Co-Routines and Networks of Parallel Processes
 Proc IFIP 77 (North Holland Pub Co 1977) pp861-867 (invited paper)
 =IDEA MATHEMATICAL TOP-DOWN SPECIFICATION LOGIC DESIGN
.Close

Parnas93
.Open Parnas93
 David Lorge Parnas
 Predicate Logic for Software Enginering
 IEEE Trans software Engineering SE-V19n9(Sep 1993)pp856-862
 =EXPERIENCE FORMAL SPECIFICATION LOGIC partial functions
.Box
Problem with partial functions in specification. example: sqrt, subscript, ...

Simple fix for engineering purposes:
 state that primitive predicates have the value false when an
argument is undefined.  A primitive predicate is one that (1) has values
defined for all defined arguments, (2) is not defined in terms of any other
predicate, (3) is false if any argument is undefined.

Not unsimilar to the Logic of Partial Terms: 
.See [LPT].

Also see 
.See [PVS]
.Close.Box
.Close

Parnas96a
.Open Parnas96a
 David Lorge Parnas
 Mathematical Methods: What we need and don't need
 IEEE Computer Magazine V29N4(Apr 1996)pp28-29
 =ESSAY MATHEMATICS ENGINEERING model description specification
.Box
not "formal" but "mathematical", as in other areas of engineering.

part of the everyday toolset

current are theoretically sound but hard to use

littered with sound foundations on which nobody has erected a useful edifice

more work on notation - current is cumbersome and hard to use.

distinguish: model, description, and specification.

unreasonable focus on proof of correctness

more tme spent applying and improving methods, not selling them,

They've been used (
.See [Parnas94]
...) but not using symbolic logic.
.Close.Box
.Close

Parnas10
.Open Parnas10
 David Lorge Parnas
 Really rethinking 'Formal Methods'
 IEEE Computer Magazine V43n1(Jan 2010)pp28-34 + letter V43n3(Mar 2010)pp6-7
 =POLEMIC =HISTORY FORMAL METHODS ASSUMPTIONS RESEARCH vs PRACTICE MATHEMATICS ENGINEERING vs PHILOSOPHY
 Claims of progress and industrial adoption doubted.
Example: benefits of inspection vs formal specification known since 1979.
They can account for most later claims!
 Alarming gaps: Research vs Practice,  Software development vs engineering, computer science and mathematics. 
 Mathematical papers are about a particular formal language not discovering ways to apply new mathematics to a problem.
 Computer variables are finite state machine but in mathematics variable are placeholders in functions and relations.
 How to handle arrays.
 Conventional expressions don't express piecewise-continuous and discrete functions.
 These days: most software variables have a hidden state., programs do not terminate, and time is important.
 Use relations and relational algebra!  Abandon pre-conditions and post-conditions!
 Work in multiple directions.
 Find ways to handle side-effects and non-determinism.
 Distinguish model vs specification vs description. Avoid "specification languages"
 Investigate using a predicate to specify requirements.
 Need to be able to analyze a program like an engineer analyses a circuit.  Not program proof,
but derivation of properties.
 Need to research ways to use mathematics to document programs -- outside of the code of the program.
 De-emphasize "technology transfer" and advocacy, instead go back and change what we are selling.
 We need an integrated notation and step by step ways of moving from user to code.
 Be careful to spot abstractions that are lies!
 Don't try to be philosophers and logicians... try to emulate engineers.
 Letter from Toomas Plaks: Some math applications were lost in the search for formal methods.
 Letter from Lee Pike: quotes examples of successful FMs, but some research not worthwhile.
 Reply: mathematics is not yet mainstream.
.Close

Parnas10a
.Open Parnas10a
 David L Parnas
 Inside RISKS: Risks of Undisciplined development
 Commun ACM V53n10(Oct 2010)pp2527- 
.See http://doi.acm.org/10.1145/1831407.1831419
 =ESSAY ENGINEERING DISCIPLINE vs SLOPPY PROGRAMMING SOFTWARE BUGS 
 Engineering designs must be fit for their purpose, conform to standards, handle all foreseeable circumstances (including human error), and be designed with a margin of error for safety.
 Anecdotes of typical problems with software.
 Proposes
.List
 First Describe all possible inputs.
 Second express requirements as disjoint sets of inputs with a common simple rule.  
 Then verify no overlaps, and each output is correct in the opinion of stakeholders.  
Use simple logic. 
 Complications: (1) often need to work with sets of sequences of inputs.
(2) Function names? (3) Output rule may be complex.
.Close.List
 Situation won't change if customers don't stop buying sloppy software.
.Close

Parnasetal94
.Open Parnasetal94
 David Lorge Parnas & Jan Madey & Michal Iglewski
 Precise Documentation of Well Structured Programs
 IEEE Trans SE VSE-20n12(Dec 1994)pp949-976
 =EXPERIENCE RISKS TABULAR RELATION DOCUMENTATION V&V
 The Darlington Project: verify safety of large atomic reactor shutdown program
 Use tables not symbolic logic.
 Specify the Before-After relationship and the conditions when it will not fail to terminate.
 a_display::=Net{ this_part_s_spec:specification; this_part_s_structure:structure; components:#specification}, shows what you need to validate a part.
.See http://www/dick/notes/Parnasetal94.html
.Close

PascalF04
.Open PascalF04
 Fabian Pascal
 Data management misconceptions 
 Government Computer News V23n9(Sep 2004)
.See http://gcn.com/23_29/interview/27383-1.html
 =INTERVIEW HARMFUL XML SQL
 XML retransmits redundant tags with each set of data transmitted.
 XML is no more than a hierarchical database when used for storage.
 XML does not provide integrity checks of a relational system.
 XML does nothing to provide the logic/mathematics provided by previous data management systems.
 SQL allows duplicated entries and empty entries in a table and so allows
errors and forces work arounds.
 SQL implementations are often incomplete and inefficient.... making it worse.
.Close

Paulos98
.Open Paulos98
 John Allen Paulos
 Once Upon a Number: The Hidden Mathematical Logic of Stories
 Basic Books NewYork NY 1998 ISBN 0-465-05158-8 QA276.P285
 =ESSAY LOGIC MATHEMATICS and story telling
 Differences between informal logic and formal logic.
 The importance of taking a point of view or placing data in a story-like context.
 Note: Software is a formal system thrown into an informal context.
 Choice can change the odds in such a way as to invalidate the choice!
 Ramsey-type theorems:  In a large enough sample even unlikely events will occur.
 The Delphi-Omni-Sci is programmed to answer any Yes/No question about the physical world correctly by outputting Yes or No.  It fails if asked if it is about to answer "No".
.Close

Paulson89
.Open Paulson89
 James D Paulson
 Reasoning Tools to Support Systems Analysis and Design
 Ph. D Thesis UBC (Main library LE3 B7 1989 A1 P38)
 =THESIS TOOLS LOGIC SELMA ANALYSIS 
.See [SELMA]
 Summarized in 
.See [PaulsonWand92]
 Systems used Turbo Prolog and suffered from a combinatorial explosion, Need for Formal model at start and tools to enable error checking.
.Close

Pawlaketal95
.Open Pawlaketal95
 Zdzislaw Pawlak & Jerzy Grymala-Busse & Roman Slowinski & Wojciech Ziarko
 Rough Sets
 Commun ACM V38n11(Nov 1995)pp89-95
 =Theory AI LOGIC SETS
 summary:
.See http://www/dick/maths/logic_31_Families_of_Sets.html#Bracketing sets
.Close

PeledGriesSchneider02
.Open PeledGriesSchneider02
 Doron A Peled & David Gries & Fred B Schneider
 Software Reliability Methods
 Springer-Verlag NY Secausus NJ(2002) $69.95 ISBN 1852335173 CR 0303-0222 D.2.4
 =TEXT FORMAL V&V SQA LOGIC LTL Buchi Hoare algebra Milner Petri sequence charts
.Close

PetersParnas00
.Open PetersParnas00
 Dennis K Peters & David L Parnas
 Requirements-based Monitors for Real-Time Systems
 Proc ISSTA 00 & ACM SIGSOFT Software Engineering Notes V25n5(Sep 2000)pp77-85
 =THEORY REQUIREMENTS LOGIC TEST TIMING ERRORS
 Mathematical specification of IN OUT REQ allow the derivation of a machine
that observes IN OUT and reports if they are OK or not.
 could be used in testing an as safety device in use.
 In practice the monitor can fail.
 compare with user tests in XP!
 Compare with 
.See [Littlewood00]
 See [PetersParnas98]
 See [PetersParnas02]
.Close

Petre95
.Open Petre95
 Marian Petre
 Why Looking isn't always seeing: Readership Skills and Graphical Programming
 Commun ACM V38n6(Jun 1995)pp33-44+letter V38n10(Oct 1995)pp19-20
 =EXPERIMENT GRAPHIC LOGIC READABILITY
 expertise in domain makes a difference in strategy and outcome.
 flawed by use of bad graphic notations rather than good ones.
 Alternatively see
.See [Scanlan89]
.Close

PettorossiProietti96
.Open PettorossiProietti96
 Alberto Pettorossi & Maurizion Proietti
 Rules and Strategies for Transforming Functional and Logic Programs
 ACM Computing Surveys V28n2(Jun 1996)pp360-414
 =Theory PERFORMANCE FUNCTIONAL LOGIC PROGRAMMING
.Close

PeytonJones86
.Open PeytonJones86
 ?? Peyton & ?? Jones
 Parsing Distfix Operators
 Commun ACM 29 2 (Feb 1986) pp118-122
 =DEMO DDD logic
.Close

PiccoRomanMcCann01
.Open PiccoRomanMcCann01
 Gian Pietro Picco & Gruia-Catalin Roman & Peter J McCann
 Reasoning about code mobility with mobile UNITY
 ACM TOSEM Trans Software Engineering & Methodology V10n3(Jul 2001)pp338-395
 =THEORY FORMAL LOGIC UNITY MOBILE AGENT CODE
.Close

Pike06
.Open Pike06
 Lee Pike 
 A Note on the inconsistent axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-triggered Algorithms"
 IEEE Trans Software Engineering  V32n5(May 2006)pp347-348 
 =CORRECTION LOGIC ERRORS TIMING PVS 
 Refers to J. Rushby's paper in IEEE Trans Software Engineering  V25n5(May 1999)pp651-660   
 Evidence that it is difficult to get axioms right,
and that social processes correct and improve them... not tools and logic.
 The axioms model the behavior of clocks.
 The PVS tool was used to test for consistency by constructing a model that satisfies the new
axioms.
.Close

Pittman93
.Open Pittman93
 Matthew Pittman
 Lessons Learned in Managing Object-Oriented Development
 Special Theme "Making OO Work" IEEE Software V10n1(Jan 1993)pp43-53
 =EXPERIENCE MANAGEMENT OBJECT-ORIENTED FSM ELH
 Page 48 Sidebar: Methods more alike than different.  Two part approach.
 Part 1: candidate classes, attributes and behaviours, class structure, object structure, class design, process architecture, Reuse.
 Part 2(itterative) : Problem analysis, Domain Analysis, Architectural principles, Archictectural strategies, logical design, physical design
 Techniques that help
 Nouns and verbs, Checklists, Relationships: aggregation+claasification, Scenarios, responsibillities and colaborators, FSM & Statecharts,  JSD ELHs for the protocols
.Close

PlatzerClarke08
.Open PlatzerClarke08
 Andre Platzer & Edmund M Clarke
 Computing Differential Invariants of Hybrid Systems as Fixed Points
 CMU CS Technical Report
.See http://reports-archive.adm.cs.cmu.edu/anon/anon/home/ftp/2008/CMU-CS-08-103.pdf
(PDF)
 =MATHEMATICS MODEL LOGIC ODEs DIFERENTIAL EQUATIONS SAFETY HYBRID PROGRAMS
 Gives a way to compute whether formula describing important properties are true for all time or not.
 [\alpha]\phi = `all states reachable thru Hybrid program \alpha satisfy \phi`.
 Formulas assembled out of terms (expression ~ expression) for relation "~".
 Directional derivative of a term t wrt to vector equation D : x_dot = \theta, \nabla[t] = \nabla t.\theta.
 Differential Invariant of a formula F depends on \nabla[D]F is the conjunction of \nabla t.\theta over all terms `t` in F.
.Close

Popper59
.Open Popper59
 Sir Karl Raymond Popper
 The Logic of Scientific Discovery
 Basic Books NY NY 1959
 =THEORY SCIENCE POSITIVITISM
 Experiements can only prove a theory wrong.
 Good experiments should be designed to risk doing the unpredicted.
.Close

Quaglia08
.Open Quaglia08
 Paola Quaglia 
 On Beta-Binders Communications 
 Montanari Festschrift pp456-472
.See [DeganoEtAl08]
 =IDEA MODEL  BIOLOGICAL CELLULAR SYSTEMS  CCS NON-SEQUENTIAL
 Instead of complementary paired actions (CCS) allows pairing of actions if they are of a compatible type.
 Defines syntax, equivalence, reductions, denotations, structural operational semantics,...
 Proves key results.
.Close

Racko95d
.Open Racko95d
 Roland Racko
 Making the Miracle Happen
 Software Development Magazine(Oct 1995)pp93+99+101
 =ESSAY adoption OBJECT-ORIENTED PROCESS STANDARDS IMPROVEMENT
 First improve your process, then adopt objects.
.Box
p93: "the first step is not to buy a C++ compiler or any other object-oriented language.  If you are going to enter a rider into the multikilometer Tour de France bicycle race, you first need to make sure he is fit. "

describes problems of average shop
.Net
 |-(Racko95d_0): find out why - perhaps its best?
 |-(Racko95d_1): sell management on the bottom line benefits of improvement(not objects)
 |-(Racko95d_2): where does the overload come from: internal and/or external
  |-(Racko95d_2a): for external. sell "market directed optimization" or some such phrase to the management to handle it; wait for died down
 |-(Racko95d_3): training
  |-(Racko95d_3.1): walkthroughs and design concepts (coupling cohesion)
  |-(Racko95d_3.2): coders get together to hash out standards
  |-(Racko95d_3.3):a common vocab  for words like: maintenance, good, design, walkthrough
 |-(Racko95d_4): teams develop goals, measurements and traceabillity methods
 |-(Racko95d_5): gather a stat base
 |-(Racko95d_6): The "market benefit phase" (objects).
.Close.Net
p101. How to handle a manager that shortens your estimates. (1) give a range of estimates: worst, best, most likely.  Be ready to explain how best and worst cases can happen. (2) break out the time needed for integration.

integration::= working design and code hierarchy so that the team can use them to connect the logic of the problem to real world, other systems, and physicla tchnology
.Close.Box
.Close

RaghuRameshwhinston02
.Open RaghuRameshwhinston02
 T S Raghu & R Ramesh & Andrew B whinston
 Representing Argumentation in Game Domains
 IEEE Computer Magazine V35n5(May 2002)pp68-70
 =SIDEBAR FORMAL MODEL ACTON GAME DIALECTIC  nonmonotonic LOGIC causality dialectic
 Gamma::=Net{fluents, actions, laws}.
 Fluents are time dependent propositions.
 Actions are made by players.
 Laws define the non-deterministic ways that actions change the fluents.
.See http://www.cs.utexas.edu/users/v1/papers/nmct.ps
Giunchiglia et al Apr 2002
 Demo of how designers can discuss the implications of the laws and modify them using defeasible logic.
.Close

Ramsay88
.Open Ramsay88
 Allan Ramsay
 Formal Methods for artificial intelligence
 Cambridge UP 1988 Q335.R35 ISBN 0-521-35236-3
 =MONOGRAPH LOGIC AI FORMAL MODAL LPC TIMING NonMonotonic \lambda-calculus
.Close

RamseyFP60
.Open RamseyFP60
 Frank Plumpton Ramsey (ed R B Braithwaite) 
 Foundations of mathematics and other Logical Essays
 Littlefield Adams, Paterson NJ 1960
 =ESSAYS PHILOSOPHY LOGIC  MATHEMATICS  TYPES PROBABILITY 
 Essays, papers, reviews, and notes dating from the 1920s.
.List
 Published
.List
 The Foundations of Mathematics 1925
 Mathematical Logic 1926
 On a Problem of Formal Logic 1928
 Note on the preceeding paper 1926
 Facts and Propositions 1927
.Close.List
 Unpublished
.List
 Truth and probability 1926
 Further Considerations 1928
 Last Papers 1928
.Close.List
  Appendix: Critical Notice of L Wittgenstein's "Tractatus Logico-Philosophicus"
.Close.List
 PM::="Principia Mathematica",
.See [WhiteheadRussell63].
 Dispenses with PM's pphilosophical
.Key axiom of reducibility
by using Wittgenstein's `Tractatus Logico-Philosophicus`.   
.Box
 PM gives a syntactic definition set of special `predicative` truth functions to avoid  paradoxes and then has to assume that all sets (for example) of objects of a given type can be expressed using one of these functions. 
 Ramsey uses a semantic definition from Wittgenstein that makes any truth function `predicative`.
.Close.Box  
 Argues for the need for a theory of types.
 Does not discard axioms of infinity and selection.
.Box
 PM's
.Key Axiom of infinity
asserts the existence of an infinite domain, Needed to define infinite numbers. 
Because, in PM, numbers measure the size of sets of objects of a particular type. 
Indeed a number is a set of all sets with the same size of that type.
So the largest number for a given type is = to the size of the type. 
 PM's
.Key Axiom of selection 
is equivalent to the Axiom of Choice
.See wikipedia 
.Close.Box
.Close

RaysideCampbell00
.Open RaysideCampbell00
 Derek Rayside & Gerard T Cambell
 Aristotle and Object-Oriented Programming: Why Modern Students Need Traditional Logic
 ACM SIGCSE Bulletin V32n1(Mar 2000)pp237-244 (Proceeding of 31st SIGCSE Technical Symposium on C Sci Education Austion Texas)
 =SURVEY traditional LOGIC OBJECT-ORIENTED
 traditional logic  is about meaning rather than formal manipulation of symbols.
 Meaning defined by a heirarchy of general and specific classification.
 Doesn't distinguish between behavioural and structural properties.
.Close

Reichenbach47
.Open Reichenbach47
 Hans Reichenbach 
 Elements of Symbolic Logic
 The Macmillan Co., NY NY. 1947 5th edition 1956 BC 135 R4
 =THEORY LOGIC LANGUAGE PHILOSOPHY   
 This book is most famous for analyzing all the tenses found in most natural languages
.See ./samples/tenses.html 
in terms of three times: S=time of Speech, R=a time Referred to, and E=time(s) when Event occurred(was occurring).
 For example "It was raining in Manchester in 1935" has S="August 2006", R is some time in 1935, and E is a range of times surrounding R when it was raining.
 If "I will see you tomorrow" is spoken on day S, then it's R is the day after S and E is a time in that day.
 Reichenbach argues that all three times: E,R and S are needed to explain all the tenses.
 He also shows that R tends to be the same inside a sentence except where it is explicitly shifted. This tends to be true across sentences as well.... except that later authors
give many counter examples where the times interact with the link: 
narrative, explanation, elaboration, etc. holding between the sentences.  

 The book is a thorough and persnickety philosophical analysis of natural language and thought in terms of symbolic logic.
 It harks back to Whitehead and Russell's `magnum opus`
.See [WhiteheadRussell63].
 It has an excellent list
.See ./samples/tautologies.html
of `true` formulas.
.Close

Ressler93
.Open Ressler93
 Sandy Ressler
 Perspective on Electronic Publishing: Standards & Solutions and more
 Prentice Hall Englewood Cliffs NJ 1993, ISBN 0-13-287491-1 
.See [CR]
9407-0424
 =TEXT WWW/NET DOCUMENTS
.Box Review
 ch1 views: visual, logical, design(fonts,...), communications(pragmatics), engineered, database
 ch2 Form and function
 ch3 Document standards SGML ODA de Facto
 ch4 Graphics and integration
 ch5 Choice
 ch6 management
 ch7 case studies
 Not enough detail, for novices, good questions, few answers
.Close.Box
.Close

Roberts73
.Open Roberts73
 Don D. Roberts
 The Existential Graphs of Charles S. Peirce
 The Hague 1973 Mouton  B945.P44 R6 
 =ADVERT GRAPHIC LOGIC
.Close

RobertsonAgusti99
.Open RobertsonAgusti99
 David Robertson & Jaume Agusti
 Software Blueprints: Lightweight Uses of Logic in Conceptual Modeling
  Addison Wesley ACM Press NY NY 1999 Order# 704992  ISBN 0-201-38919-2 
.See [CR]
0001-0008
 =MONOGRAPH LOGIC Prolog MODELS ANALYSIS DESIGN PROOFS BSDM SIMULATION SKELETONS Argumentation Temporal SYNTAX SEMANTICS
 network:= Net{ R:=requirements:Sets, P:=Positions:Ssets, issues:Sets, D: decisions:Sets, specialize:@(R, R), generate:@(R, I), adopted_in_response_to:@(P, I), suggest:@( I, P), based_on:@(D, P), resolve:@(D, I), depend_on:@(D, D) }.
.See [RameshLuqi93]
 (dick)|- `Use Prolog notation.  Solutions assume perfect typing!`.
 abduction, induction, deduction.  defeasible logics.  can_not_be_shown ( P  ). argumentation. endorsement.
 Systems dynamics models - (dick)|- `inadequate numerical method`
 BSDM ::=`Existence dependency model`.
 Example: maintaining www pages!
.Close

RobinsonjPurao09
.Open RobinsonjPurao09
 William N Robinson & Sandeep Purao
 Specifications and Monitoring Interactions and commitments in Open Business Processes
 IEEE Software Magazine V26n2(Mar/Apr 2009)pp72-79
 =IDEA SERVICE BUSINESS PROCESS MODEL UML SEQUENCE DIAGRAMS OCL TEMPORAL LOGIC REQUIREMENTS MONITORING
 When many different components and/or actors provide services to each other ... with the network being
dynamically configured, one must define the interactions precisely and monitor to see if they
are being followed.  For example, after a bill is sent to a customer, one expects to be paid...
 UML Sequence charts can show the protocols: patterns of messages.
 Add to this 
.Key conditional commitments (CC)
with four parts
.List
 The actor who is committed to bring something about: customer.
 The actor who expects the the commitment: biller.
 The statement that becomes true: customer send payment.
 The conditions under which it becomes true: the biller billed the customer.
.Close.List
 Proposes a temporal logic extension to the OCL with clause like "after time until time...", "always....", "never ...", "eventually ...",
 By using existing logging service we can monitor the interactions and collect information on how well
commitments are being kept.
 Then see
.See [RobinsonWN10]
.Close

RobinsonWN10
.Open RobinsonWN10
 William N Robinson
 A roadmap for comprehensive requirements monitoring
 IEEE Computer Magazine V43n5(May 2010)pp64-72 
 =IDEAS  MONITORING REQUIREMENTS COMPLEX SYSTEMS BAM FEEDBACK OCL  TEMPORAL LOGIC 
 Overly complex attempt at a universal theory of monitoring systems to see if they are fulfilling requirements.
 BAM::="business activity monitoring". 
 Model user requirements and compare with the streams of the events that occur. 
 Based on
.See [RobinsonjPurao09]
.Close

Roetzheim00
.Open Roetzheim00
 William Roetzheim
 Estimating Software Costs
 Software Development Magazine V8n9(Oct 2000)pp66-68
 =TUTORIAL COCOMO COSTS KSLOC
 Effort: PersonMonths = a* KSLOC^p, where a & p depend on project. a in 2.5..3.60, p in 1..1.2.
  SLOC by sum of module estimates using mean = ( bet + worst  + 4*expected)/6, sd =( worst - best )/6
 or by function points (fp) based on number of inputs*4 + files*7 + outputs*5 + queries*4 +  logical database tables*10.
 sloc = c * fp, c depends on the language.
.Close

Rosen00
.Open Rosen00
 Keneth H Rosen(editor in chief)
 Handbook of discrete and combinatorial mathematics
 CRC Press Dnvers NY 2000 ISBN 0-8493-0149-1 QA164.H36 1999
 =REFERENCE LOGIC DISCRETE MATHEMATICS ALGORITHMS GRAPHS
.Close

Rushby97a
.Open Rushby97a
 John Rushby
 Subtypes for Specifications
 in 
.See [JazayeriSchauer97]
pp4-19
 =EXPERIECE LOGIC PREDICATES TYPES
 useful to use predicate to define subtypes an use subtypes in quantifiers etc in logic in specifications+proofs+assertions+functions
 Tool = 
.See [PVS]
 Also see 
.See [RushbyOwreShankar98]
.Close

RushbyHenke92
.Open RushbyHenke92
 John Rushby & Friedrich von Henke
 Formal Verification of Algorithms for Critical Systems
 ACM SIGSOFT'91 Conf on Software for Critical Systems: Software Eng Notes V16n5(Dec 1991)pp1-15, republished IEEE Trans SE-19n1(Jan 1993)pp13-23
 =EXPERIENCE PROOF CHECKER LOGIC EHDM Z
 EHDM - the "implacable sceptic"
.Box
 need for a proof checker with library of reusable theories including both discrete and concrete mathematics - the "implacable sceptic" forcing you to express all assumptions, found errors in published work, typos in Z specification, corrected and simplified publishable proof of a complex real time algorithm, able to rapidly do 'what ifs', productive symbiosis, tools: editor, parser, typechecker, browesers, cross-referenceers,...typographical output, a sort of module structure for specifications, first order logic with a fragment of higher order logic (functions of functions), 19 axioms and 200 proofs

ICA problem as a challenge

Need reusable library of theories

Need a type theory which distinguishes similar algebras like velocity vs length or real time vs clock time.
.Close.Box
.Close

RushbyOwreShankar98
.Open RushbyOwreShankar98
 John Rushby & Sam Owre & Natarajan Shankar
 Subtypes for Specifications:  Predicate Subtyping in PVS
 IEEE Trans SE V24n9(Sep 1998)pp709-720
 =THEORY LOGIC partial 
.See [PVS]
 Also see 
.See [Rushby97a]
 Compare 
.See [Parnas93]

.Close

SaariluomaIsomki08 
.Open SaariluomaIsomki08 
 P Saariluoma & H Isomki 
 Future interaction design ii (1st ed.)
 Springer Publishing Company, Incorporated, 2008 $CR 1003-0249
 =THEORY =EXPERIMENT =SURVEY PHILOSPHY USER HCI SOCIOLOGY GERONTECHNOLOGY ANTHROPOLOGY
 Intro+9 papers
.List
 Need to replace folak lore by science.
 Gerontechnology
 Virtual vs real -- 3 experiments
 Need to combine technological and psychological models. Monitor cognitive load and modify.
 partial history of scientific psychology in design.
 History of HCI experiments. Mobile devices must be tested outside.
 SUX::="service user experience". 
 locative media. Urban. Actor-network theory ANT constructivist.
 technology acceptance  vs appropriation 
 purpose and meaning continuously redefined by users. Anthopology.
 need holistic view of human. Modes of being. Phenomenology. Metatriangulation.
.Close.List
 No ref to
.See [Dwyer81]
!
.Close

Sain92
.Open Sain92
 Ildiko Sain
 Temporal Logics and their Clocks
 Theor Comput Sci V95n1(Mar 23 1992)pp75-95 CR9303-0168(M Abadi)
 =Theory Logic Concurrent
.Close

Schaefer06
.Open Schaefer06
 Robert Schaefer 
 A Rational theory of System-making systems
 ACM SIGSOFT Software Engineering Notes V31n2(Mar 2006)p31 (online supplement pp1-20)
 =ESSAY LARGE SYSTEMS FAILURE DILBERT =SURVEY SOCIOTECHNICAL PEOPLE POWER PLANS PROGRAMS PROCESSES POLITICS BUREAUCRACY 
 Large projects/systems tend to fail for complex endemic sociological reasons.
 A key problem: separating the planner/designer/thinker from the doer. 
The plan/design can not handle all the contingency and the doer
is forbidden to be creative when handling the unexpected.
 For more see
.See [Dumay06]
on BPR in conflict with people.
.Close

Schaefer07
.Open Schaefer07
 Robert Schaefer
 The Grand Theory of Everything: What Man-Made Systems are, and Why They Fail
 ACM SIGSOFT Software Engineering notes V32n4(Jul 2007)p31
.See http://doi.acm.org/10.1145/1281421.1281430
(links to a 26 page PDF)
 =JOKE? THEORY FAILURE tGToE
 tGToE::="the Grand Theory of Everything".
 Written in an 18th century Style -- with Many `definitions` and Random Capitalizations
but Getting Close to Heart of the Reason for Complex Systems Failing.
 Here is a Cogent Quotation from the Verbose and Jocular Paper:
.Box
In the practice of Systems Development, Rules are enumerated to comprise a
Finite sized Set of Constraints. This Set in Systems Development is called
the Requirements (in Systems Use these are called Policies). The number of
Freedoms that a System has is the Inverse of that Finite Set of Constraints
which by Rules of Logic are Infinite in number. This relationship of Finite
Rules and Infinite Freedoms is more than a Curiosity, as in the mapping of
a Solution into a Model of Behavior, the Rules become Contractual Shalls (A
"Shall" being a Statement that Indicates a Contractual Obligation of Legal
Consequence) while the Inverse, Freedoms, become the Infinite Set of "Shall
Nots. That Infinite Set of Shall Not Behaviors represents a Set which can 
never be Fully Imagined, and thus can never Fully Defined, Implemented, or
Tested. Because this Set can never be Fully Defined it is customarily 
Replaced with a Time and Money based Stopping Criteria, i.e. to Proceed 
along the set of Requirements (that One hopes is at least a "well-defined"
Subset of Infinity) until the Requirements are Implemented and Tested, or 
the Customer's Will as measured by Time and Money, Runs Out. Note that at 
this Stopping Point there may be a Gap between "What Is", and "What Is 
Desired". In terms of Systems Reliability, this Gap is called a Hazard.
.Close.Box
 To summarize: requirements are always incomplete and some conditions
will always be untested.
 Also see
.See [Schaefer06]
and
.See [Gall79].
.Close

SchiederBroy99
.Open SchiederBroy99
 Birgit Schieder & Manfred Broy
 Adapting calculatonal logic to the Undefined
 Computer Journal V42n2( 1999)pp73-81
 =THEORY LOGIC MATHEMATICS FORMAL
 Dijkstra, Gries, no ref to 
.See [Parnas93]
 Shows three value: true, false and undefined calculus which allows recursive definitions via a Fixed point rule of inference.
.Close

SchneiderK04
.Open SchneiderK04
 Klaus Schneider
 Verification of Reactive Systems: Formal Methods and Algorithms
 Springer-Verlag London UK 2004 ISBN 3540002960 $CR 0409-1013
 =THEORY FORMAL V&V ALGORITHMS MODEL CHECKING Borel FIXPOINT AUTOMATA MODAL LOGIC
.Close

SchnuppBernhard87
.Open SchnuppBernhard87
 Petter(?) Schnupp & Lawrence W. Bernhard
 Productive Prolog Programming
 Carl Hanser Verlag and Prentice Hall International(UK) 1987
 =HOWTO PROLOG logic-programming DDD JSP Reality
.Close

Schock69
.Open Schock69
 R Schock
 Logics without Existence Assumptions
 Almqvist & Wikells 1968 Stockholm Sweden
 =THEORY FORMAL LOGIC
 See 
.See [LPT]
and 
.See [LPV]

.Close

Scott76
.Open Scott76
 Dana S Scott
 Logic and Programming Languages
 Turing Award Lecture 1976
.See [ACM86]
 =AUTOBIOGRAPHY =MATHEMATICS INTRODUCTION SCOTT FUNCTION SPACES LATTICES POSETS SEMANTICS
 Provides a semantics for typeless \lambda calculus.
.Close

Selic00
.Open Selic00
 Bran Selic
 A generic framework for modeling resources with UML
 IEEE Computer Magazine V33n6(Jun 2000)pp64-69
 =MODEL QoS OMG UML PERFORMANCE MODEL
 distinguish logical model from the engineering (physical) model.
.Close

Shanahan97
.Open Shanahan97
 Murray Shanahan
 Solving the Frame Problem: A Mathematical Investigation of the common sense law of inertia
 MIT Press Cambridge MA 1997 ISBN 0-262-29384 
.See [CR]
9802-005
 =THESIS AI LOGIC FRAMES INERTIA
.Close

Shankar93
.Open Shankar93
 A Udaya Shankar
 An Introduction to Assertional Reasoning for Concurrent Systems
 ACM Computer Surveys V24n3(Sep 1993)pp225-262
 =Tutorial concurrency fairness safety non-sequential temporal logic
 Prereq for LamShankar94 & Jonsson94...
 refers to Lamport, UNITY, Mana et al
.Close

ShankarAsa03
.Open ShankarAsa03
 Subash Shankar & Sinan Asa
 Formal Semantics of UML with Real-Time Constructs
 LNCS 2863 <<UML>> 2003 -- The Unified Modeling Language Oct 2003, pp60-75
 =THEORY SEMANTICS TIMING UML SEQUENCE STATECHARTS TEMPORAL LOGIC PTL
.Close

Shao10
.Open Shao10
 Zhong Shao 
 Certified Software
  Commun ACM V53n12(Dec 2010)pp56-66  
.See http://doi.acm.org/10.1145/1859204.1859226
 =IDEAS DEPENDABLE CORRECT PROOF CHECKER ASSEMBLER MACHINE CODE TOOLS EXAMPLES Coq METALOGIC FUNCTIONAL NONSEQUENTIAL 
 Minimize the components that can damage the dependability of the system. 
 Both proofs and specifications can be represented by executable programs. Example using CoQ
(Wikipedia)|- Coq implements a dependently typed functional programming language...
.See en.wikipedia.org/wiki/Coq
 "huge cost in constructing ... specifications and proofs"
 Dynamic validation - add a check after an unproved step and use a proved component if the check fails. 
 "time to market is likely terrible"
 PCC - proof-carrying code -  give executable code with a proof of safety to a host that checks the proof. 
 Proof checking is automated and about as difficult as type checking. 
 FPCC - Foundational PCC.
 CAP - certified assembly programming - using a mechanisable Metalogic. 
 Modular reasoning. Separation logics. CSL - concurrent separation logic. 
 Domain specific logics. 
 There exist certified garbage collectors, thread libraries, compilers, and certifying compilers, 
etc.
 (dick)|-How to handle changing requirements and specifications?  Can proofs be agile?
.Close

Shin95
.Open Shin95
 Sun-Joo Shin
 The Logical Status of Diagrams
 Cambridge U Press UK 1995 $39.95 197+pages
 =THEORY GRAPHIC LOGICS
.Close

SiddiqiShekaran96
.Open SiddiqiShekaran96
 Jawed Siddiqi(Sheffield Hallam U UK) & M Chandra Shekaran(MS)
 Requirements Engineering: The Emerging Wisdom
 IEEE Software magazine V13n3(Mar 1996)pp15-19
 =EDITORIAL REQUIREMENTS ENGINEERING
 introduction to special theme articles pp20-64
 RE::=systems analysis with engineering orientation
 effect of context+need to handle changing context+questioning what.vs.how
and the functional.vs.nonfunctional + problem frames and repetoire of 
methods( Jackson95)+anthopological approach + non-contractual forms of 
requirements(no one-size)
.Close

SiffReps99
.Open SiffReps99
 Michael Siff & Thomas Reps
 Identifying Modules via Concept Analysis
 IEEE Trans Software Engineering V25n6(Nov/Dec 1999)pp749-768
 =THEORY =DEMO EVOLUTION MODULES C to C++ LOGIC TOOL
 Improves on Snelting's work
.See [Snelting96]
.See [SneltingTip98]
 Use function vs struct attributes.
 Concept partition:=modules where each function linkd to one module. may need to add attributes. include negative information.
 Tested on SPEC 95 benchmark, case studies on chull and bash
.Close

SmithA90
.Open SmithA90
 Alf Smith
 The Knuth-Bendix Completion Algorithm and its Specification in Z
 pp195-220 in 
.See [Nicholls90]
 =DEMO SPECIFICATION Z Mathematics vs Logic
 cf 
.See [NelsonOppen80]
.Close

SobelClarkson02
.Open SobelClarkson02
 Ann E Kelley Sobel & Michael R Clarkson
 Formal methods application: An Empirical Tale of Software Development
 IEEE Trans Software Engineering  V28n3(Mar  2002)pp308-320 +  Correspondence (Beery & Tichy) V29n6(Jun 2003)pp567-575
 =EXPERIMENT FORMAL NONSEQUENTIAL LOGIC SPECIFICATION DERIVATION METRICS UML lift problem  c++ MFC
 Compared formally vs informally developed programs by students for controlling elevators.nn E Kelley Sobel & Michael R Clarkson 
 Formal methods application: An Empirical Tale of Software Development
 IEEE Trans Software Engineering  V28n3(Mar  2002)pp308-320 +  Correspondence (Beery & Tichy) V29n6(Jun 2003)pp567-575
 =EXPERIMENT FORMAL NONSEQUENTIAL LOGIC SPECIFICATION DERIVATION METRICS UML lift 
problem  c++ MFC 
  Methods first order logic, UML diagrams,pseudocode, 
  differences: formal group 100% functional vs <50% of the informal groups. most formal groups handed in UML vs no informal groups did.
 Similarities.  No statistically significant difference in conciseness and complexity of code,
 Includes a  formal solution of one algorithm developed after the experiment by some of the students.
 Daniel M Berry & Walter F Tichy wrote following,
.Net
 Glad that somebody did some empirical research.
 Self selected groups weaken result.
 Hawthorne and Novelty also weaken result.
 No knowledge of what happened in "control" groups.
 Correctness results based on very few test cases.
 No discussion of external threats to validity.
 Sobel & Clarkson replied  following,
.Net
 Educational research (teaching formal methods) is not an industrial or lab experiement.
.Close.Net
.Close.Net
.Close

SotirovskiKruchten95
.Open SotirovskiKruchten95
 Drasko M Sotirovski & Phillipe B Kruchten
 Implementing Dialogue Independence
 IEEE Software Magazine(Nov 1995)pp61-70
 =DEMO MODULES ARCHITECTURE PATTERNS HCI USER HIDE LOGIC 
 separation of user interface and core application by using glue objects for existence properties and transitions
 `glue` is like a two-way version of the Observer pattern.
 Compare with class type architecture and many others
.Close

SowmyaRamash98
.Open SowmyaRamash98
 Arcot Sowmya & S Ramash
 Extending Statecharts with Temporal Logic
 IEEE Trans SE V24n3(Mar 1998)pp216-231
 =DEMO DYNAMICS STATECHARTS TEMPOAL MODAL LOGIC
 FNLOG::="Logic-Based Function Specification Language".
.Close

Spivey89
.Open Spivey89
 J Michael Spivey
 The Z Notation: A reference Manual
 Prentice Hall Series in C Sci 1989(UK)
 =handbook formal logic
 Later see
.See [Spivey01]
(online)
.Close

Spivey92
.Open Spivey92
 J Michael Spivey
 The Z Notation: A Reference Manual
 Prentice Hall Series in C Sci 1992(UK) ISBN 0-13-978529-9 CR 9307-0424(D.2.1)
 =handbook formal logic
 Earlier was
.See [Spivey89]
later on the web
.See [Spivey01]
as PDF.
.Close

Spivey01
.Open Spivey01
 J M Spivey 
 The Z Notation: A Reference Manual (online)
 Web 2001 
.See ./samples/zrm.pdf
.See http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf
 =handbook formal logic Z SPECIFICATION
 
 Earlier citations/versions
.See [Spivey89]  
.See [Spivey92] 
.Box Quote from web site
.See http://spivey.oriel.ox.ac.uk/mike/zrm/index.html

The Z Reference Manual has now been allowed to go out of print by the 
publisher, Prentice Hall, but they have kindly returned the copyright to 
me, so I can make the full text available here.

Please note that I have not placed the copyright of this work in the public
domain. Nevertheless, I freely grant permission to make copies of the whole
work for any purpose except direct commercial gain. I retain all other 
rights, including but not limited to the right to make translations and 
derivative works, and the right to make extracts and copies of parts of the
work. Fair quotation is permitted according to usual scholarly conventions.
.Close.Box
.Close

SpohrerRiecken06
.Open SpohrerRiecken06
 Jim Spohrer & Doug Riecken (Eds) 
 Service Science (Special Issue/Section)
 Commun ACM V49n7(Jul 2006)pp30-87
 =SURVEY =ADVERT RESEARCH CONSULTANCY SERVICE INDUSTRY ECONOMICS SSME 3S WEB2.0 CRM
 Introduction + 12 articles/papers 
 p33: 55 references.   
 If you divide the economy in agriculture, manufacture, and service then most of it is now service!
 Even when selling product, service can make the difference.
 This change means that research and education needs to develop (or at least) shift to a focus on service rather than production.
 SSME::="Services Science, Management, and Engineering".
 Service implies:
.Box
 Expertise and knowledge by the supplier.
 But the suppliers knowledge must be fitted to customers specific environment.
 Services are a socio-technical system and not a pure technological fix.
 Need to model/understand the people and organization of the customer.
 Exchange of service for something of value.
 Negotiation, interaction, and trust between customer and supplier.
 Long term relations with customers.
 Communication is vital.
 Service often encoded as software+hardware --algorithmic.
 3S:="An ontology describing services: humans, web, software, ..." 
 Innovation and perhaps revolution in the enterprise.
 New courses and schools.
.Close.Box
 (dick)|- with luck they will rediscover systems analysis and operations research from the 1950s.
.Close

StepanovMcJones09
.Open StepanovMcJones09
 Alexander Stepanov & Paul McJones
 Elements of Programming
 Addison-Wesley Professional (June 09, 2009) Print ISBN: 0-321-63537-X Web ISBN 0-321-64392-5 Safari $CR 1105-0457
.See http://www.elementsofprogramming.com/book.html
 =TEXT THEORY C++ PROGRAMMING FORMAL LOGIC MATHEMATICS ALGORITHMIC CODE GENERIC ABSTRACTION ADT 
.Close

Stephenson07
.Open Stephenson07
 Peter Stephenson 
 AMenaza SecuriTree has a different view of Risk Analysis
 CS Magazine for Security Professionals, (Feb 2007)p67     
 =REVIEW TOOL Fault trees LOGIC SECURITY REQUIREMENTS RISK ANALYSIS Amenaza SecuriTree  
 See
.See http://www.amenaza.com 
.Close

Stevens95
.Open Stevens95
 Anthony Stevens
 Review of "Information Modeling: Specification and Implementation" (Edmond92)
 Comp Rev V36n1(Jan 1995)p62 
.See [CR]
9501-0017
 =REVIEW REFINEMENT Z SQL
 "[...]impression that SQL had become integrated with[...]Z
 What unifies the two fields are the basic concepts of discrete mathematics - sets, relations, functions, and logic. [...] training materials for a systems nalysis courses with a modern flavore[..]well-thought-out and extensive examples[...] humor[...]"

"[Refinement...] it appears that this part of formal methods continues to be a kind of mental torture. When we specify formally, we seem to say so much with so little, whereas when we refine, we seem to achieve so little with so much."
.Close

StrawsonOderberg05
.Open StrawsonOderberg05
 P Strawson & David S Oderberg Eds.
 The old new logic: Essays on the philosophy of Fred Sommers
 MIT Press Cambridge MA ISBN 0262151138 CR 0710-0977
 =UNREAD Aristotle Syllogism TERMS TLP vs MPL PREDICATE
 TLP::="Term Functor Logic".
 Instead of predicates, facts are expressed in terms like [-S+C]+[W+S]-[W+C].
 Simplifies many arguments that are complex in LPC.
.Close

StubblebineWright02
.Open StubblebineWright02
 Stuart G Stubblebine & Rebecca N Wright
 An Authentication Logic with Formal Semantics Supporting Synchronization, Revocation, and Recency
 IEEE Trans Software Engineering  V28n3(Mar  2002)pp256-285
 =THEORY LOGIC TEMPORAL BELIEF DISTRIBUTED TIME PROTOCOLS BAN web certificates Kerberos5
.Close

Sutton00
.Open Sutton00
 Stanley M Sutton Jr.
 The Role on processes in a Software start-up
 IEEE Software Magazine V17n3(Jul/Aug 2000)pp33-39
 =ESSAY EXPERIENCE ECCubed ORGANIZATION PROCESS
 if startup then inexperienced and lmited resources and multiple changing constraints 
and changing technologies and need speed and small.
 Define but remain flexible using suitable techniques for most useful subprocesses.
 Generalize. generic procedures and technological infrastructure.
 Learn from experiences. Only define reusable procedures.
 Hire competent techical people and superstar managers.
.Close

Tayloretal96
.Open Tayloretal96
 Richard N Taylor & Nenad Medvidovic & Kenneth M Anderson & E James Whitehead Jr. & Jason E Robbins & Kari A Nies & Peyman Oreizy & Deborrah L Dubrow
 A Component- and message- based Architectural Style for Gui Software
 IEEE Trans Softw Eng VSE22N6(Jun 1996)pp390-406 revised from ICSE-17 1995
 =DEMO Chiron2/C2 decomposition ARCHITECTURE COMPONENT MESSAGE NONSEQUENTIAL MODULES
 Compare with
.See [RajlichSilva96]
 layered modules of two types: components and connectors.
 decoupling: Connector<->component<->connector...
 message::= request|notification.
 layers(like onion with logical ADTs in center).
 requests flow in and notifications out.
 Notifications are not necesarily acted on.
.Close

Terwilliger93b
.Open Terwilliger93b
 Robert W Terwilliger <terwilli@cs.colorado.edu>
 An Example of Process Verification: the Gries/Dijkstra Design Process
 ACM SIGSOFT Software Engineering Notes V18n3(Jul 1993)ppA26-35
 =CASE-STUDY V&V CORRECTNESS FORMAL LOGIC DESIGN PROOF
.Close

ThimblebyLadkin96
.Open ThimblebyLadkin96
 Harold Thimbleby & Peter Ladkin
 From logic to manuals
.See http://www.cs.mdx.ac.uk/Harold/papers/log2manop.html
 =DEMO TOOL LOGIC LANGUAGE TABULAR DOCUMENTATION WWW Manuals
 Shows how to prepare manuals with boolean expressions that are automatically, indexed, linked, and converted into tables.
.See http://www/dick/notes/ThimblebyLadkin96.html
.Close

ThimblebyLadkin97
.Open ThimblebyLadkin97
 H. W. Thimbleby & P. B. Ladkin
 From Logic to Manuals Again
 IEE Proceedings Software Engineering, 144(3),pp185-192, 1997
 =DEMO LOGIC DOCUMENTATION TLA FSM/STD HCI
 Compare 
.See [ThimblebyLadkin96]
.Close

Thomas90
.Open Thomas90
 Automata on Infinite Objects
 in 
.See [Leeuwen90]
pp133-187
 =THEORY MODEL MODAL LOGIC TEMPORAL Buchi AUTOMATA FSM/STD
.Close

Tillman93
.Open Tillman93
 George Tillman
 A Practical Guide to Logical Data Modelling
 McGraw-Hill Inc New York NY 1993 ISBN 0-07-064615-5
 CR9411-0772 
.Close

Toulmin58
.Open Toulmin58
 Stephen Edelston Toulmin  
 The uses of argument.
  Cambridge [Eng.] University Press, 1958 BC177
 =THEORY INFORMAL LOGIC ARGUMENT RATIONALE
 Developed into text
.See [ToulminRiekeJanik78]
.Close

ToulminRiekeJanik78 
.Open ToulminRiekeJanik78 
 Stephen E Toulmin & Richard Rieke & Allan Janik
  An introduction to reasoning 
  Macmillan, c1979.  New York  BC177 .T59
 =TEXT INFORMAL LOGIC ARGUMENT RATIONALE GRAPHIC
 Based on
.See [Toulmin58]
 Toulmin_argument::=data "--->" O(qualifier) claim ", " warrant O(backing) O(rebuttal) .
.As_is         Backing
.As_is           | 
.As_is        Warrant 
.As_is           |
.As_is Data -------------> (Qualifier) Claim
.As_is                          |
.As_is                       Rebuttal
 Toulmin_argument::=following
.Net
 Claim::Utterance, conclusions
 Data::Utterance, facts
 Warrant::Utterance, general rule linking the data to the claim.
 Backing::Utterance, credentials when the warrant is not convincing enough.
 Rebuttal::Utterance,  restrictions which apply to the claim. 
 Qualifier::Phrase, possibly, likely, probably, certainly, presumably, necessarily.
.Close.Net
.But
.See [Loui08]
.See [HaleyLaneyMoffettNuseibeh08]
.Close.But
.Close

Tremblay99
.Open Tremblay99
 Guy Tremblay
 Exercises for Teaching Logic in a Formal Methods Course: Formalizing ERDs
 ACM SIGCSE Bulletin -- Inroads V31n1(Mar 1999)pp100-104
 =DEMO Spec
.Close

TsaiWiegertJang92
.Open TsaiWiegertJang92
 Jeffrey J P Tsai & Thomas Weigert & Hung-chin Jang
 A Hybrid Knowledge Representation as a Basis of Requirement Specification and Specification Analysis
 IEEE Trans SE-V19n12(Dec 1992)pp1076-1100A
 =SUVEY FRORL LOGIC FORMAL SPECIFICATION OBJECT-ORIENTED non-monotonic hierarchy
.Box
 ORIENTED non-monotonic hierarchy(general with exceptions) frames for objects and activities complete and sound.
 Compare Kaindl93 arguing for frames to support informal preparations.

Section I Introduction(pp1076-1077)
 p1076: "Software development usually begins with an attempt to recognize and understand the user's requirements[...] Software developers are always forced to make assumptions about the user's requirements[...] Often the user has an incomplete understanding[...]"
Goguen and Meseguer's work on FOOP 1987 (Functions+objects+relational methods)
 p1077: "an_instance_of", "a_kind_of", "a_part_of". "formal correctness checking is desirable[...]surpass the expressiveness of standard first order logic"... "complete and sound with respect to these semantics[Horn clause logic+nonmonotonicity]. [...] the users can automatically analyze various properties of a FRORL specification."

Section II Demands(pp1077-1078)
 p1077 "domain model[vs]specification" "theorems [---] facts"

Section III The language(pp1078-1081)
 p1078 "Given an informal description of the problem domain" operational and decalrtive interpretations possible.
 p1079 Refers to Booch91 and Kowalski's book

Section IV Semantic foundations(pp1081-1085)
 Predicates and Consistency (\para_symbol) statements, Horne clauses, Herbarnd interpretations, fixed points of a theory operator. some model theoretic semantics. Some computational procedure to indicate if a clause is a logical consequence of a theory

Section V Mapping FRORL into Semantics(pp-)

Section V Analysis of specifications(pp1085-1090)
 reachability, reversibillity, liveness, and consistency. State space or problem reduction. Use abstracted attributes.

Section VII Software Environment(pp1090-1093)
	Sun SparcStation Open Look

Section VIII Related work (pp1093-1096)
	Survey based on Wing88. Mentions with KATE, CAKE, LARCH, Ina Jo, GIST, SASCO, PLEASE, SXL,...

Section IX Conclusions and plans(pp1096)

Section X. Appendix BNF(pp1096-1097)

Section XI Appendix B Soundness and Completeness (pp1097-1099)

54 References (pp1099-1100)
.Close.Box
.Close

TuckerNoonan02
.Open TuckerNoonan02
 Allen B Tucker & Robert E Noonan
 Integrating Formal Models into the Programming Language Course
  SIGCSE'02 Proceeding & ACM SIGCSE Bulletin V34n1(Mar 2002)pp346-350
 =EXAMPLE FORMAL SPECIFICATION J
 denotational semantics implemented with objects(Java), functions(Scheme), and logic(Prolog)
 Note. the OO implementation is like Botting99
.Close

Turpin93
.Open Turpin93
 Russell Turpin<turpin@cs.utexas.edu>
 A logical Approach to Data Structures
 In
.See [Notkin93] pp138-148
 =THEORY DATA STRUCTURES PROOF POINTERS
.Box
Part of Texas Adv Res Proj, admin J C Browne.

Formal development and verification of data structure programs. pointers and destructive update.

"well known to programmers but they are usually informally defined by the programming community or operationally defined in particular imperative languages" NO!: implementations.
Concepts: data structures address, pointer reference, data structure disjointness, data structure isomorphism.

"gap between the formalisim that was provided and the way in which the problem area is naturally discussed... common textx on formal verification omit pointers from their prescription for programming.

Predicates
	PartOf(x,y), 
	Dangles(p,x) ::=`p is not NULL but x has no part with address p`,
 HasDangles(x), Navigable(x), Disjoint(y,x), y":"":"x

Status: prototype compiler, graphical interface, mapping to standard theprem prover, incomplete....environment enforces a greater attention to invariants, details, and exceptional conditions. Debugging moved to compile time. out-of-bounds suscripts and mangled pointers are eliminated.

records See [1] Beeri Catriel et al "Embedding \Psi- terms in a Horn-clause Logic Language" MCC Tech Report ACA-ST-050-88.

objects See [12] MaierD86, "A Logic for Objects" In Proc o t Workshop on the Foundations of Deductive Databases and Logic Programming, Washington DC, Aug 1986 pp6-26.

Galois programs specified in logic: name, modes for arguments, goal predicate, precondition - no unification or clausal search required.
Composition generates proof obligations: Prerequisite asssertion
.Close.Box
.Close

TyszberowiczYehudai92
.Open TyszberowiczYehudai92
 Shmuel Tyszberowicz & Amiram Yehudai
 OBSERV -- A Prototyping Language and Environment
 ACM Trans Softw Eng Methodol V1n3( Jul 1992 )pp 269-309
 =THEORY RAD GRAPHIC OBJECTS CONCURRENCY LOGIC PROGRAMMING STDs/FSMs
 - no backend
.Close

Vadaparty06
.Open Vadaparty06
 Sirisha Vadaparty
 Semantic Tableaux Program
 CSUSB CSci Master Project 2006
.See http://csci.csusb.edu/dick/seminar/20060222SirishaVardaparty.txt
 =DEMO LOGIC PROOF TOOL TREE CASES LPC Java
.Close

vanBenthem97
.Open vanBenthem97
 Johan van Bentham
 Exploring Logical Dynamics
 Center for Study of Lang and Info Stanford CA 1997 ISBN 1-57586-059-7 $59.95 CR9712-0979
 =MATHEMATICS LOGIC RELATIONS DYNAMICS
.Close

Venture78
.Open Venture78
 Alec Venture
 Loglan -- a more flexible language
 =LETTER Esperanto vs Loglan Volapuk LOGIC  ITL UNIVERSAL LANGUAGES
 Computer Weekly (UK) (Mar 23 1978)p19
 Rebuts Taylor78 and Botting78a.
.Close

VesseyWeber86
.Open VesseyWeber86
 Iris Vessey & Ron Weber
 Structured Tools and Conditional Logic: An Empirical Investigation
 Commun ACM V29n1(Jan 1986)pp48-57
 =EMPIRICAL STRUCTURED SEQUENTAL SP LOGIC GRAPHICS
 different representations for different purposes
 overall superiority of decision trees vs linear sequence of program language text
 compare
.See [Petre95]
.Close

WangBastaniYen05
.Open WangBastaniYen05
 Dongfeng Wang & Farokh B Bastani & I.-Ling Yen
 Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance
 IEEE Trans Software Engineering  V31n9(Sep 2005)pp713-732
 =IDEA MATHEMATICS MODAL LOGIC TLA ASPECTS COMPONENTS NONDETERMINISTIC FSM RHSM IDEAL BART
.Close

WandWeber90
.Open WandWeber90
 Yair Wand & Ron Weber
 An Ontological Model of an Information System
 IEEE Trans SE-16n1(Nov 1990)pp1282-1291
 =THEORY SYSTEM Formal Mathematics Systems decomposition
.Close

WangBastaniYen05
.Open WangBastaniYen05
 Dongfeng Wang & Farokh B Bastani & I.-Ling Yen
 Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance
 IEEE Trans Software Engineering  V31n9(Sep 2005)pp713-732
 =IDEA MATHEMATICS MODAL LOGIC TLA ASPECTS COMPONENTS NONDETERMINISTIC FSM RHSM IDEAL BART
.Close

WardM96
.Open WardM96
 Martin Ward
 Derivation of Data Intensive Algorithms by Formal Transformation: The Schnorr-Waite Graph Marking Algorithm
 IEEE Trans SE V22n9(Sep 1996)pp663-686
 =THEORY LOGIC SPECIFICATION DERIVATION ALGORITHM DATA
 action language with specification statements
 steps introduce ghost variables
 steps can combine data structures that both drive and are developed by the algorithms
.Close

Warnier76
.Open Warnier76
 Jean Dominique Warnier
 The Logical Construction of Programs
 Out of print. see pp 85-105 of ParikhZvegintzov82
 =HANDBOOK =CLASSIC TECHNICAL DESIGN LCP DDD
 Bracketted notation. Data structures first, then operations, then place ops in data.
 Source for the Warnie-Orr methods.
 Compare JSP.
.Close

Warnier81
.Open Warnier81
 Jean Dominique Warnier
 Logical Construction of Systems
 Van Nostrand Reinhold NY NY 1981
 =SURVEY LCS data
 Follows
.See [Warnier76].
.Close

WeberWeisbrod03
.Open WeberWeisbrod03
 Mathias Weber & Joachim Weisbrod
 Requirements Engineering in Automotive Development: Experiences and Challenges
 IEEE Software Magazine V20n1(Jan/Feb 2003)pp16-24
 =EXPERIENCE REQUIREMENTS TOOLS PROCESS DaimlerChrysler 
 tools
.List
 DOORS::="Dynamic Object Oriented  Requirements System",
.See http://www.telelogic.com/Products/doors/doors/index.cfm
(was Telelogic, now IBM).
 RequisitePro::=http://www.rational.com/products/reqpro.
 RTM::="Requirements Traceability and Management",
.See http://www.chipware.com/
.Close.List
 Complex domains have complex requirements.
 Requirements are more than text. Text+data(state, ...) +graphics... +metadata.
 Engineers and customers live in a document-driven world that has to be reflected in tools.
 Need to distinguish what the customer wants(Laastenheft) from what the supplier is contracted to do(Pflichtenheft).
 Redundancy causes problems but is built in to the existing system.
 Good engineers are already content specialists in their special area and the content tends to evolve incrementally, so it pays to recycle old specifications.
 Takes time to migrate documents into a new requirements database.
 Details only appear at the leaves of the tree. 
 Nonfunctional requirements, acceptance criteria and tests are not done well.
 Change is part of project life.  Be ready to handle a lot of it.
 User-adaptable views help guide and manage a process.
 Specification reviews are important.
 Traceability is good: but what should be traced?
 Bad couplings between tools and text.
 We need better tools to manage requirements.
  Most of the problems are in areas that are not being researched.   The real problem is managing the complexity not in expressing content and domain knowledge. 
.Close

Weideetal94b
.Open Weideetal94b
 Bruce W Weide & William F Ogden & Marli Sitaraman
 Recasting Algorithms to Encourage Reuse
 IEEE Software Magazine V11n5(Sep 1994)pp80-88
 =ESSAY ALGORITHMS REUSE MACHINES
.Box
 Algorithm becomes machine(state+smaller effect operations) ??virtual machine?? encapsulated objects and hidden objects.
 p82: "this basic idea has neither been touted as being as general as it is nor been further developped and systematically applied to the design of reusable software"
 p82: recasting a sort: "there are two distinct phases: and insertion phase and an extraction phase" (just like COBOL)
 "In our design neither the data's source nor its destination must be a certain data structure"
 p85: "Edges previuosly extracted could be made erroneous as new edges are inserted. This additional reason supports the logic behind making this a two-phse machine" (there is an order clash)(assembly line diagram of Orr).
 p87: "Machine-oriented design is easier for clients understand"
 p88:"First try to develop a simple, fully abstarct, clearly explainable mathematical model. Then consider if you can settle for a two-phase mahine. You should probably have a two phase version of every machine in the reusable component library even if you can't see the immediate need for it in a particular case. Often, implementations for two-phase machines are easier to and/or potentially more efficient than for multiphase or haeless machines."...
 choose a design that is easily explained.... "what and when your machine does something will depend, in part, on which explanation is most understandable. You might have to use trial and error before you can judge which is best. But don't worry about the initial cost of making these design decisions! If you component is really reusable, the effort you spend on making a good design choice will be amortized over many future uses."
.Close.Box
.Close

Weidenbach95
.Open Weidenbach95
 Christoph Wiedenbach
 First-Order Tableaus with Sorts
 PostScript file Downloaded from internet, Max-Planck-Institue fur Informatik, Im Stadtwald, 66123 Saarbruken, Germany
 =THEORY LOGIC SEMANTIC TABLEAUX TREES TYPES
 demonstrates that tableaus - treestyle proofs - are shortened by adding types(sorts) as a special set of unary predicates and modfying two rules. The result is complete and sound.
.Close

Weidenback94
.Open Weidenback94
 Christoph Weidenbach
 First-Order Tableaux with Sorts
 Submitted to IGPL usenet group June 1995 ftp://dcs.ox.ac.uk/sorttab.ps.g(??)
 =THEORY LOGIC SEMANTIC TABLEAUX TREES TYPES
.Box
Gensen style natural induction (cf hodges) extended by adding sorts to variables,
 Each variable has a set of sorts assoicated with it.
 Each sort is interprtted as a unary predicate.  s(x)=finite@(U->@)...
	for all x (p) +> for all x ( if and(s(x)(x)) then p).
	for some x (p) +> for some x ( and(s(x)(x)) and p).
Modified derivation rules
	for all x (p(x)), and( s(x)(t) ), t any term |- P(t)

	for some x (p(x)), new v |- p(v), and( s(x)(v) )

Gives much simpler proofs

Proved to be as complete and consistent as the original

.Close.Box
.Close

Wells95
.Open Wells95
 Charles Wells
 Communicating Mathematics: Useful Ideas from Computer science
 Am Math Monthly V102n5(May 1995)pp397-408
 =ESSAY MATHEMATICS 
.Box
function Doamain->Bool as external behavior
 Sets are a way to represent other things.
 specify external behavior rather than set theoretic representations when introducing ideas.

Distinguish syntax from semantics: expression vs what it denotes, ainformal parsing, make types explicit

Formal transformations: definitions as macros, proof by rewriting(GriesSchneider95), give syntactic and semantic proof., mental representations, make logic explicit.

Types and polymorphism. distinguish function, its vlaues, an algorithm that implemnts it.

Self-montoring:give mistakes a name. give punchy names for good behaviours, go for high context communitcation
.Close.Box
.Close

Whangetal92
.Open Whangetal92
 Kyu-Young Whang & Ashok Malhotra & Gary H Sockut & Luanne Burns & Key-Sun Choi
 Two-Dimensional Specification of Universal Quantification in a Graphical Database Query Language
 IEEE Trans SE-18n3(Mar 1992)pp216-224
 =ADVERT GRAPHIC DATA LOGIC
.Close

WhiteheadRussell63
.Open WhiteheadRussell63
 Alfred North Whitehead & Bertrand Russell 
 Principia Mathematica(2nd Edition) Vol 1
 OUP UK: Oxford University Press England 1963
 =CLASSIC logic RELATIONS SETS PREDICATES structures regular TYPES
 dotty notation and fun typographical symbols.
 Attempting to show that the whole of mathematics is a subset of formal logic.
 To resolve paradoxes introduced the theory of types.
 To make type system work invented generic expressions "Typical ambiguity".
 Interesting model of induction and the theory of "..." via transitive closures.
 Republished as
.See [WhiteheadRussell97]
.Close

WhiteheadRussell97
.Open WhiteheadRussell97
 Alfred North Whitehead & Bertrand Russell 
 Principia Mathematica to *56
 Cambridge University Press UK1997
 =FORMAL LOGIC TYPES PREDICATES CLASSES RELATIONS PROOFS MATHEMATICS  
 Facsimile of the beginning of the original 1927 `magnum opus` going from the propositional calculus to the definition of the numbers 0, 1, & 2!
 PM::="Principia Mathemtica by Russell and Whitehead, 1927, ... ".
 Attempts to construct traditional mathematics in formal symbolic logic.
 Earlier edition
.See [WhiteheadRussell63]
from Oxford University Press.
.Close

WidomGriesSchneider92
.Open WidomGriesSchneider92
 Jennifer Widom & David Gries & Fred B Schneider
 Trace-based Network Proof Systems: Expressiveness and Completeness
 ACM Trans Program Lang Syst(TOPLAS)V14n3(Jul 1992)pp396-416 CR9302-0090
 =THEORY CONCURRENT SNL=Simple Network Logic
 Predicates over traces, sound but incomplete, needs the addition of temporal ordering and prefix properties.
.Close

WilsonF00
.Open WilsonF00
 Fred Wilson
 The Logic and methodology of science and pseudo-science
  Canadian's Scholars Press Inc, Toronto Ont CA 2000 ISBN 1-55130-175-X Q175.W66 2000
 =FORMAL LOGIC SCIENCE HISTORY THEORY DATA
.Close

WingNixon89
.Open WingNixon89
 Jeanette M Wing & M R Nixon
 Extending Ina Jo with Temporal Logic
 IEEE trans on Soft Eng SE-V15n2(Feb 1989)pp181-197
 =ADVERT formal specification
.Close

WingVaziri-Farahani95
.Open WingVaziri-Farahani95
 Jeanette M Wing<wing@cs.cmu.edu> & Mandana Vaziri-Farahani
 Model checking software systems: A Case study
 in 
.See [Kaiser95]
 =CASE-STUDY SQA FORMAL CASE-STUDY LOGIC
 It is feasible to check for some properties of non-finite state systems.
 When does ( p(a) imply (for all x(p(x))))?
.Close

Woodcock89b
.Open Woodcock89b
 JCP Woodcock
 Calculating Properties of Z Specifications
 ACM SIGSOFT Software Engineering Notes v14n5(Jul 1989)pp43-54
 =DEMO MATHEMATICS Z formal logic structures
.Close

Wordsworth96
.Open Wordsworth96
 J B Wordsworth
 Software Engineering with B
 Addison-Wesley Longman Reading MA 1996 ISBN0-201-40356-0 CR9709-0632(D.2.1)
 =TEXTBOOK undergraduate TOOLs B MATHEMATICAL LOGIC
.Close

Wos98
.Open Wos98
 Larry Wos
 Programs that offer Fast Flawless Logical Reasoning
 Commun ACM V41n6(Jun 1998)pp87-95
 =ADVERT LOGIC TOOL not AI but rules and algebra
 OTTER::=http://www.mcs.anl.gov/home/mccune/ar/
 database+inference+paramodulation+hyperresolution etc
 p93: "axiomatization" and representation in the program's language can be trying& even formidable
.Close

XiaLee0
.Open XiaLee0
 Weidong Xia & Gwanhoo Lee
 Grasping the Complexity of IS Development projects
 Commun ACM V47n5(May 2004)pp69-74
 =POLL COST TIME USER FUNCTION NONTECHNICAL
  distinguishes organizational from technological Complexity.
 Finds organizational complexity has the most effect.
.Close

Yamazakietal93
.Open Yamazakietal93
 Seichi Yamazaki & Kiyohiko Kajihara & Mitsutaka Ito & Ryuichi Yasuhara
 Objected-oriented Design of Telecommunication Software
 Special Theme "Making OO Work" IEEE Software V10n1(Jan 1993)pp81-87
 =EXPERIEMENT OBJECT-ORIENETD ROOD Real-time vs FD
 Object models==<{logical model, integration model} vs Physical model,
 Static(ER)+dynamic(FSM)+message sequences,
 Case study compared OO(in Ada 83)+FD on 10K LOC: OO gave greater extendabillity,
 lesser performance,
 more smaller and simpler modules (No inheritance),
 difficult to grasp the entire model and check consistency.
.Close

YangHawblitzel11
.Open YangHawblitzel11
 Jean Yang & Chris Hawblitzel
 Safe to the last instruction: Automated verification of a type-safe operating system
  Commun ACM V54n12(Dec 2011)pp123-131
.See http://doi.acm.org/10.1145/2043174.2043197
 =ADVERT LOGIC PROOF TOOLS SAFETY MEMORY OSs Kernel Nucleus  Typed Assembly Language TAL Verve Hoare C#
 Demonstrates feasibility of developing a proved type-safe operating system.
.Close

Young97
.Open Young97
 William D Young
 Comparing Varification Systems: Interactive Consistency in ACL2
 IEEE Trans Softw Eng VSE23n4(Apr 1997)pp214-223
 =DEMO PROOF LOGIC LISP 
.See [ACL2]

.See [KaufmanMoore97]
hardware CLI
 advantages of no types and LISP-like notation vs 
.See [PVS]
Rushby
.Close

Young07
.Open Young07
 Chelsea Anne Young
 Spreadsheets using logic instead of math may revolutionize data management
 =ADVERT LOGIC TOOL
 Standford Logic Group
.See http://news-service.stanford.edu/news/2007/april25/logic-042507.html
 Quote "There are many cases where traditional spreadsheets are just not 
sufficient," says Associate Professor Michael 
.Key Genesereth
, whose group in 
the Computer Science Department is developing this new method of data 
management. "Why not have a spreadsheet that looks just like a regular 
spreadsheet except it has the ability to encode and use logical formulas? 
That's what you can't do with Excel in any way today."
.Close

Yourdon07
.Open Yourdon07
 Ed Yourdon
 Celebrating Peopleware's 20th Anniversary
 IEEE Software Magazine V24n5(Sep/Oct 2007)pp96-100
 =HISTORY PEOPLE =REPORT PANEL Boehm Brooks Rising Lister DeMarco
 The major problems with software development are sociological not technical.
.Close

Zadeh94
.Open Zadeh94
 Lotfi A Zadeh
 Fuzzy Logic, Neural Networks, and Soft Computing
 Comm ACM V37n3(Mar 1994)(AI issue)pp77-86
 =ADVERT FUzzY LOGIC
.Close

ZaveJackson93
.Open ZaveJackson93
 Pamela Zave<pamela@research.att.com> & Michael A Jackson
 Conjunction as Composition
 ACM Trans on Softw Eng & Meth V2n4(Oct 1993)pp379..411 CR9408-0546
 =DEMO FORMAL REQUIREMENTS SPECIFICATION
.Box
Note Multi-paradigm specifications, more in Jackson95x

Must have common semantics.  So assume first order logic. Model types as one-place predicates. Kleene's notation..., Z , prolog,....

Renaming to couple and instanciate specifications.

Distinguish defined from undefined terms.
 ?? Problem with recursive predicate definitions
Must form a DAG

statements equivalent to
.As_is 		for all p:Projects, one m:EMPLOYEE(m leads p).
member(x,y) := x \in y

sequences modeled as totally order sets of events.

Net{member::@event, preceeds::@(event,event)... initial, final,...}
.Close.Box
.Close

ZaveJackson96
.Open ZaveJackson96
 Pamela Zave<pamela@research.att.com> & Michael A Jackson
 Where Do Operations come From? A Multiparadigm Specification Technique
 IEEE Trans Soft Eng VSE-22n7(Jul 1996)pp508-528
 =DEMO specification methods logic std Z
 better than 
.See [ZaveJackson9X]
 
.See [ZaveJackson93]
.Close

ZaveJackson9X
.Open ZaveJackson9X
 Pamela Zave & Michael A Jackson
 Where Do Operations come From? Specification of Event Properties
 Preprint received Pamela Zave 1993 - Submitted for publication 1993.  Published as 
.See [ZaveJackson96]
 =DEMO Multiparadigm specification GRAPHIC Z STDs Jackson diagrams predicate LOGIC
 sequences input events occurring at multiple events need to be mapped into central operations in a central specification
 incomprehensible graphical notation for case analysis(fig 4) is not  in 
.See [ZaveJackson96]
.Close

ZellerSnelting97
.Open ZellerSnelting97
 Andreas Zeller & Gregor Snelting
 Unified Versioning through Feature logic
 ACM ToSEM V6n4(Oct 1997)pp398-441
 =THEORY =TOOLS SCM
 feature logic defined in Smolka92 J Logic Programming
.Close

Zelkowitz94
.Open Zelkowitz94
 Marvin V Zelkowitz<mvz@cs.umd.edu>
 Algebra and Models ( and Reality)
 ACM SIGSOFT Software Engineering Notes v19 n10(Oct 1994 1995)pp79-81 & V20 n4 (Apr 1995)pp55-57
 =CRITIQUE HOARE LOGIC PROGRAM
 States the algebra of Hoares algebra of programs
 quotes 
.See [Hoare69]
and Hoare in 1993
 argues that since on some machines x'=x+1 does not implie x'>x on all machines that modern mathematics shouldn't be used.
 Appeals for a (as yet) unknown approach based on natural science.
 "There needs to be feedback"
.Close

Zhang91
.Open Zhang91
 Guo-Qiang Zhang
 Logic of Domains
 Birkhauser Boston Inc Cambridge MA 1991 ISBN 0-8176-3570-X CR9303-0126(D.2.2)
 =THEORY Semantics SFSS SFP.
 cpos<==SFP<==scott<==stable domains.
.Close

ZowghiOffen97
.Open ZowghiOffen97
 Didar Zowghi & Ray Offen
 A Logical Framework for Modeling and Reasoning about the Evolution of Requirements 
 RE'97 pp247-257
.See [RE'97]
 =THEORY REQUIREMENTS EVOLUTION AGM
 nonmonotonic logics |~ epistemic entrenchement AGM
.Box
.See [Gadenfors88]
P Gardenfors, Knowledge in Flux: Modeling the Dynamics of Epistemic States'.
MIT Cambridge MA 1988
.Close.Box
.Close

Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

To see the complete bibliography (1Mb+) select:[Bibliography]