CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1.

Timothy E. Lindquist, Roy F. Keller

Research output: ResearchChapter

  • 2 Citations

Abstract

Two relations of the weakest precondition function are given. The first defines the sequential execution of two program statements. The second defines concurrent execution of two program statements in terms of buffering range variables and the relation for sequential execution. The statement types of the language KL-1 are given along with their operational semantics. A weakest precondition function is defined for each of these statement types. Finally it is shown, by using the sequential and concurrent relations, and the weakest precondition functions defined, how programs written with simple variables using the constructs of KL-1 can be demonstrated to be logically correct.

LanguageEnglish (US)
Title of host publicationUnknown Host Publication Title
Place of PublicationNew York, NY
PublisherIEEE
Pages635-639
Number of pages5
StatePublished - 1800
Externally publishedYes
EventCOMPSAC '77, IEEE Comput Soc Int Comput Software & Appl Conf, 1st, Proc - Chicago, IL, USA
Duration: Nov 8 1977Nov 11 1977

Other

OtherCOMPSAC '77, IEEE Comput Soc Int Comput Software & Appl Conf, 1st, Proc
CityChicago, IL, USA
Period11/8/7711/11/77

Fingerprint

Semantics

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Lindquist, T. E., & Keller, R. F. (1800). CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1. In Unknown Host Publication Title (pp. 635-639). New York, NY: IEEE.

CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1. / Lindquist, Timothy E.; Keller, Roy F.

Unknown Host Publication Title. New York, NY : IEEE, 1800. p. 635-639.

Research output: ResearchChapter

Lindquist, TE & Keller, RF 1800, CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1. in Unknown Host Publication Title. IEEE, New York, NY, pp. 635-639, COMPSAC '77, IEEE Comput Soc Int Comput Software & Appl Conf, 1st, Proc, Chicago, IL, USA, 11/8/77.
Lindquist TE, Keller RF. CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1. In Unknown Host Publication Title. New York, NY: IEEE. 1800. p. 635-639.
Lindquist, Timothy E. ; Keller, Roy F./ CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1.Unknown Host Publication Title. New York, NY : IEEE, 1800. pp. 635-639
@inbook{80abdec39c1e4194a8d0e25960f46550,
title = "CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1.",
abstract = "Two relations of the weakest precondition function are given. The first defines the sequential execution of two program statements. The second defines concurrent execution of two program statements in terms of buffering range variables and the relation for sequential execution. The statement types of the language KL-1 are given along with their operational semantics. A weakest precondition function is defined for each of these statement types. Finally it is shown, by using the sequential and concurrent relations, and the weakest precondition functions defined, how programs written with simple variables using the constructs of KL-1 can be demonstrated to be logically correct.",
author = "Lindquist, {Timothy E.} and Keller, {Roy F.}",
year = "1800",
pages = "635--639",
booktitle = "Unknown Host Publication Title",
publisher = "IEEE",

}

TY - CHAP

T1 - CORRECTNESS OF PROGRAMS WRITTEN IN THE LANGUAGE KL-1.

AU - Lindquist,Timothy E.

AU - Keller,Roy F.

PY - 1800

Y1 - 1800

N2 - Two relations of the weakest precondition function are given. The first defines the sequential execution of two program statements. The second defines concurrent execution of two program statements in terms of buffering range variables and the relation for sequential execution. The statement types of the language KL-1 are given along with their operational semantics. A weakest precondition function is defined for each of these statement types. Finally it is shown, by using the sequential and concurrent relations, and the weakest precondition functions defined, how programs written with simple variables using the constructs of KL-1 can be demonstrated to be logically correct.

AB - Two relations of the weakest precondition function are given. The first defines the sequential execution of two program statements. The second defines concurrent execution of two program statements in terms of buffering range variables and the relation for sequential execution. The statement types of the language KL-1 are given along with their operational semantics. A weakest precondition function is defined for each of these statement types. Finally it is shown, by using the sequential and concurrent relations, and the weakest precondition functions defined, how programs written with simple variables using the constructs of KL-1 can be demonstrated to be logically correct.

UR - http://www.scopus.com/inward/record.url?scp=0017792450&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0017792450&partnerID=8YFLogxK

M3 - Chapter

SP - 635

EP - 639

BT - Unknown Host Publication Title

PB - IEEE

ER -