Topic: Cleanroom software development
Topic: flow diagrams and flow charts
Topic: logic programming
Topic: mathematical proof
Topic: mobile code
Topic: program proof via assertions
Topic: programming without errors
Topic: proofcarrying code
Topic: transformation of programs
 
Subtopic: constructive proof
Quote: Euclid's algorithm for greatest common divisor; with proof [»eucl_300, OK]
 Quote: geometric construction of equilateral triangles; with proof [»eucl_300, OK]
 Quote: rigorous, detailed, readable specification from realworld traces of three implementations of the TCP/IP protocols and Sockets API; verified with a symbolic model checker [»bishS1_2006]
 Subtopic: proof as part of programming
Quote: a program and its proof should be developed together; with the proof usually leading the way [»grieD_1981]
 Quote: formality is important in programming because of the large amount of detail which must be absolutely correct [»grieD_1981]
 Quote: instead of program verification should derive correct programs with correctness checked at each stage [»scheWL9_1983]
 Quote: should develop program and its correctness proof together [»mannZ7_1979]
 Quote: correctness proof and program should be written together [»dijkEW10_1972]
 Quote: must develop a program and its correctness proof together; better to derive a correct program than to have a direct correctness proof [»baueFL_1976]
 Subtopic: human reasoning
Quote: writing new code is natural with reference immutability; helped define interfaces; easier than annotating existing code [»birkA10_2004]
 Subtopic: specification
Quote: describe a routine accurately; include preconditions, postconditions, validity conditions, accuracy, time taken, and method [»turiA3_1951]
 Subtopic: verification
Quote: verification gives programmers a language for understanding the program as it is written; important explanations become assertions [»bentJ10_1983]
 Quote: formal semantics enables compiletime optimization, analysis, and verification
 Subtopic: logical derivation
Quote: write programs as a specification in firstorder predicate calculus and incrementally refine it into a program [»hehnEC2_1984]
 Quote: it is more natural to describe a program by its derivation or evolution from specifications [»scheWL9_1983]
 Quote: every program is a transition axiom specification; a compiler translates the program's explicit and implicit state functions [»lampL1_1989]
 Subtopic: assertion
Quote: a programmer should make assertions that imply a correct routine; then checking the assertions checks the routine [»turiAM6_1949]
 Quote: assist a program checker with a table of assertions for each state of the machine with restrictions on the induction variables, and the next states [»turiAM6_1949]
 Subtopic: trust management
Quote: SD3 trust management computes answer and verified proof together; only certified evaluator in trusted computing base; e.g., a secure name service [»jimT5_2000]
 Subtopic: eventbased model
Quote: a verification model must identify control states, event types, and event responses as code fragments [»holzGJ5_1999]
 Subtopic: memory model
Quote: a program includes global, local, and induction variables; only local and induction (the bound variables) may use shared storage; [»goldHH_1948, OK]
 Subtopic: loop invariant
Quote: it is important to find the loop invariant for each loop [»grieD_1981]

Related Topics
Topic: Cleanroom software development (38 items)
Topic: flow diagrams and flow charts (21 items)
Topic: logic programming (34 items)
Topic: mathematical proof (23 items)
Topic: mobile code (14 items)
Topic: program proof via assertions (61 items)
Topic: programming without errors (28 items)
Topic: proofcarrying code (7 items)
Topic: transformation of programs (27 items)
