A contour image representation is stated and an algorithm for

converting a set of digital television images into this

representation is explained. The algorithm consists of five steps:

digital image thresholding, binary image contouring, polygon

nesting, polygon smoothing, and polygon comparing. An implementation

of the algorithm is the main routine of a program called CRE;

auxiliary routines provide cart and turn table control, TV camera

input, image display, and xerox printer output. A serendip

application of CRE to type font construction is explained. Details

about the intended application of CRE to the perception of physical

objects will appear in sequels to this paper.

We consider the power of several programming features such as counters,

pushdown stacks, queues, arrays, recursion and equality. In this study

program schemas are used as the model for computation. The relations

between the powers of these features is completely described by a

comparison diagram.

The maximum, minimum and average computing times of the classical

Euclidean algorithm for the greatest common divisor of two integers are

derived, to within codominance, as functions of the lengths of the two

inputs and the output.

This report describes a system of programs which perform natural

language processing based on an underlying language free

(conceptual) representation of meaning. This system is used to

produce sentence paraphrases which demonstrate a form of

understanding with respect to a given context. Particular emphasis

has been placed on the major subtasks of language analysis (mapping

natural language into conceptual structures) and language generation

(mapping conceptual structures into natural language), and on the

interaction between these processes and a conceptual memory model.

This paper (based on a keynote address presented at the

,

Boston, October 1-3, 1973) presents the view that a programming

language is a tool which should assist the programmer in the most

difficult aspects of his art, namely program design, documentation,

and debugging. It discusses the objective criteria for evaluating a

language design, and illustrates them by application to language

features of both high level languages and machine code programming.

It concludes with an annotated reading list, recommended for all

intending language designers.

This paper develops some ideas expounded in [1]. It distinguishes a

number of ways of using parallelism, including disjoint processes,

competition, cooperation, communication and "colluding". In each

case an axiomatic proof rule is given. Some light is thrown on traps

or ON conditions. Warning: the program structuring methods described

here are not suitable for the construction of operating systems.

Defining the semantics of programming languages by axioms and rules

of inference yields a deduction system within which proofs may be

given that programs satisfy specifications. The deduction system

herein is shown to be consistent and also deductive complete with

respect to Hoare's sustem. A subgoaler for the deductive system is

described whose input is a significant subset of Pascal programs

plus inductive assertions. The output is a set of verification

conditions or lemmas to be proved. Several non-trivial arithmetic

and sorting programs have been shown to satisfy specifications by

using an interactive theorem prover to automatically generate prrofs

of the veification conditions. Additional components for a more

powerful verficiation system are under construction.

We present various heuristic techniques for use in proving the

correctness of computer programs. The techniques are designed to

obtain automatically the "inductive assertions" attached to the loops

of the program which previously required human "understanding" of the

program's approaches: one in which we obtain the inductive assertion

by analyzing predicates which are known to be true at the entrances

and exits of the loop (top-down approach), and another in which we

generate the inductive assertion directly from the statements of the

loop (bottom-up approach).