Imagen de Portada
Código QR

Proving Program Termination.

The article discusses methods for testing whether a computer program will terminate or not. This involves methods of coping with a mathematical problem that was proved to be formally undecidable by the pioneering computer scientist Alan Turing. It is known as the halting problem, or program terminat...

Descripción completa

Publicado en:Communications of the ACM Vol. 54; no. 5; pp. 88 - 99
Autores principales: COOK, BYRON, PODELSKI, ANDREAS, RYBALCHENKO, ANDREY
Formato: Artículo
Publicado: Association for Computing Machinery May2011
Materias:
Computer software termination
Decidability (Mathematical logic)
Ramsey theory
Computable functions
Computer logic
Mathematical logic
Acceso en línea:Ver este registro en EBSCOhost
Sumario:The article discusses methods for testing whether a computer program will terminate or not. This involves methods of coping with a mathematical problem that was proved to be formally undecidable by the pioneering computer scientist Alan Turing. It is known as the halting problem, or program termination problem. Although a yes or no answer cannot always be supplied, the article presents a method, based on Ramsey theory, which provides yes or no answers often enough to be useful. The method can be scaled up to large programs by constructing modular termination arguments.