Topic: constructing proof and program together

topics > computer science > programming > Group: program proving

Cleanroom software development
flow diagrams and flow charts
logic programming
mathematical proof
mobile code
program proof via assertions
programming without errors
proof-carrying code
transformation of programs
Subtopic: constructive proof up

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 real-world 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 up

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 up

Quote: writing new code is natural with reference immutability; helped define interfaces; easier than annotating existing code [»birkA10_2004]

Subtopic: specification up

Quote: describe a routine accurately; include preconditions, postconditions, validity conditions, accuracy, time taken, and method [»turiA3_1951]

Subtopic: verification up

Quote: verification gives programmers a language for understanding the program as it is written; important explanations become assertions [»bentJ10_1983]
Quote: formal semantics enables compile-time optimization, analysis, and verification

Subtopic: logical derivation up

Quote: write programs as a specification in first-order 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 up

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 up

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: event-based model up

Quote: a verification model must identify control states, event types, and event responses as code fragments [»holzGJ5_1999]

Subtopic: memory model up

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 up

Quote: it is important to find the loop invariant for each loop [»grieD_1981]

Related Topics up

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: proof-carrying code (7 items)
Topic: transformation of programs
(27 items)

Updated barberCB 7/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.