Topic: Goldstine and von Neumann consistency proof

topics > computer science > programming > Group: program proving

binding names to variables or expressions
consistency testing
flow diagrams and flow charts
machine code and assembly language


Goldstine and von Neumann's flow charting technique included a consistency proof for induction loops. Computer operations change the name of storage locations, for instance, the location 'i' could become 'i+1' during an increment operation. Substitution boxes would rename these variables and change a consistency level number. At loop interfaces location names and consistency levels must match. Alternative boxes were used for loop exit conditions, followed by an assertion box. For instance at the end of a loop on 'i', 'i' could be relabeled 'N'. (cbb 5/80)
QuoteRef: goldHH_1948 ;;91 constancy intervals between transition points "where changes of the content of any variable storage or of the value or domain of variability of any bound variables take place"
QuoteRef: goldHH_1948 ;;92 substitution boxes for changing bound induction variables (eg setting i to i+1
QuoteRef: goldHH_1948 ;;92 assertion boxes for constraining bound variables (eg i is N at the end of a loop)
QuoteRef: goldHH_1948 ;;94 storage table of location values-- must be same over constancy interval
QuoteRef: goldHH_1948 ;;94 the results of an operation are given a name and places in a storage location
Quote: in von Neumann's flow diagrams, storage only changes across operations; otherwise just consistent substitutions, assertions, and alternatives
[»goldHH_1948, OK]

Related Topics up

Topic: binding names to variables or expressions (10 items)
Topic: consistency testing (60 items)
Topic: flow diagrams and flow charts (21 items)
Topic: machine code and assembly language
(49 items)

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