| 
|
QuoteRef: redeDH7_1979
topics >
all references >
Topic:
program proof via assertions
Topic:
predicate transforms
ThesaHelp:
references p-r
Topic:
error safe systems
Group:
repetitive control
Topic:
recursion
Topic:
initialized constants
Topic:
variables as objects which remember a value
Topic:
named constants and expressions
Topic:
definition languages
Topic:
primitive data types for Thesa
Topic:
using a description as a name
Topic:
requirement specification by assertion
Topic:
global declarations and variables
Topic:
replacement as defining a variable
Topic:
parameters as argument place holders
Topic:
restricted use of global variables
Topic:
assigning values to statements
Topic:
expression language
Topic:
programming as mathematics
Group:
program proving
Reference
Redelmeier, D.H., "Eliminating the variable from Dijkstra's mini-language", University of Toronto, Computer Systems Research Group, CSRG-104, July 1979. Google
Other Reference
Stanford Computer Library #12945
3 ;;Quote: Hehner's 'if' statement is more robust than Dijkstra's 'do' because it fails if no guard is true, e.g., an unexpected state
3+;;Quote: can implement Dijkstra's 'do' statement via recursive calls of Hehner's 'if' statement
4 ;;Quote: a named constant (assign-once) can replace most variables except for repetition state
5 ;;Quote: repetitive control requires some way to record state; uses a invocation parameter that acts as a named constant
6 ;;Quote: a named constant is defined exactly once; any expression involving name constants has a fixed value as long as they are defined
7 ;;Quote: a refinement's name is also its precise specification; so prove that refinement matches its name
7+;;Quote: while proving a refinement, assume that a call does what its name promises
7 ;;Quote: the name of a refinement includes its precondition, its assignments to global variables, and an optional postcondition
7+;;Quote: a refinement is an assignment to a global named variable
8 ;;Quote: example of the weakest precondition for a simple assignment statement
8 ;;Quote: a postcondition is true after a statement; the canonical postcondition most restricts the state
10 ;;Quote: parameters carry values into refinements; global named constants carry values out
11 ;;Quote: global named constants are "wired in"; prevents multiple calls to a refinement
11 ;;Quote: a sequence of statements followed by an expression, has the value of the expression in the statements' context
11+;;Quote: ban side effects by disallowing global named constants; allows expression refinements to be used more than once in a scope
11 ;;Quote: example of writing a recursive expression refinement for factorial
11 ;;Quote: can replace inheritance of global named constants with parameters and results
11+;;Quote: can replace statement refinements by assigning the result of an expression refinement
15 ;;Quote: simplified the semantics of Dijkstra's mini-language, while increasing its expressiveness
15+;;Quote: refinement naming convention allows a new verification technique
Topic: program proof via assertions (61 items)
Topic: predicate transforms (7 items)
ThesaHelp: references p-r (245 items)
Topic: error safe systems (75 items)
Group: repetitive control (7 topics, 117 quotes)
Topic: recursion (16 items)
Topic: initialized constants (12 items)
Topic: variables as objects which remember a value (10 items)
Topic: named constants and expressions (21 items)
Topic: definition languages (3 items)
Topic: primitive data types for Thesa (82 items)
Topic: using a description as a name (21 items)
Topic: requirement specification by assertion (28 items)
Topic: global declarations and variables (33 items)
Topic: replacement as defining a variable (8 items)
Topic: parameters as argument place holders (15 items)
Topic: restricted use of global variables (22 items)
Topic: assigning values to statements (7 items)
Topic: expression language (13 items)
Topic: programming as mathematics (27 items)
Group: program proving (10 topics, 310 quotes)