Specialised theorem-proving in an intelligent tutoring system for the Dijkstra-Gries programming methodology

Author

Ng, F.C.N. ; Butler, G.

Author_Institution

Dept. of Comput. Sci., Sydney Univ., NSW, Australia

fYear

1993

fDate

27-29 May 1993

Firstpage

294

Lastpage

298

Abstract

Ego is a goal-oriented intelligent tutoring system for disciplined programming (E.W. Dijkstra, 1976), strictly following the methodology in D. Gries´s (1981) monograph for simultaneously developing a program and its proof of correctness. It contains utilities to manipulate arithmetic and logical expressions, a weakest precondition calculator, models of students´ understanding, and theorem-proving facilities, as well as knowledge of the semantics of the programming language, steps of the methodology, and theorems relevant to proofs of correctness. We report on the theorem-proving facilities. They are specialised to the programming methodology and to the tutoring system

Keywords

computer science education; intelligent tutoring systems; program verification; programming; theorem proving; user modelling; Dijkstra-Gries programming methodology; Ego; arithmetic expressions manipulation; correctness proofs; disciplined programming; goal-oriented intelligent tutoring system; logical expressions manipulation; methodology steps; program development; programming language semantics; specialised theorem proving; student understanding modelling; weakest precondition calculator; Arithmetic; Australia; Automatic control; Computer languages; Computer science; Education; Intelligent systems; Testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computing and Information, 1993. Proceedings ICCI '93., Fifth International Conference on

Conference_Location

Sudbury, Ont.

Print_ISBN

0-8186-4212-2

Type

conf

DOI

10.1109/ICCI.1993.315360

Filename

315360