ARGUS/V: A SYSTEM FOR VERIFICATION OF PROLOG PROGRAMS.

Tadashi Kanamori; Hiroshi Fujita; Hirohisa Seki; Kenji Horiuchi; Machi Maeji

ARGUS/V: A SYSTEM FOR VERIFICATION OF PROLOG PROGRAMS.

Tadashi Kanamori, Hiroshi Fujita, Hirohisa Seki, Kenji Horiuchi, Machi Maeji

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The verification system Argus/V for proving properties of Prolog programs is outlined by contrasting verification with testing in logic programming. Specifications in Argus/V are given by a class of first-order formulas, including goals for normal execution. The specification states a partial property of the program that states what the program does as a whole. Though verification in Argus/V does not guarantee the correctness of the program at one stroke, the more properties of the program proved the closer the program is to what the authors intend. Verification in Argus/V is done using inference rules. Execution in Prolog, on which testing is based, is a special case of the inferences in the verification.

Original language	English
Title of host publication	Unknown Host Publication Title
Editors	Harold S. Stone
Publisher	IEEE
Pages	994-999
Number of pages	6
ISBN (Print)	0818607432
Publication status	Published - Dec 1 1986
Externally published	Yes

All Science Journal Classification (ASJC) codes

Engineering(all)

Cite this

@inproceedings{bfaaa00613994dd7bddad110d70f8cfa,

title = "ARGUS/V: A SYSTEM FOR VERIFICATION OF PROLOG PROGRAMS.",

abstract = "The verification system Argus/V for proving properties of Prolog programs is outlined by contrasting verification with testing in logic programming. Specifications in Argus/V are given by a class of first-order formulas, including goals for normal execution. The specification states a partial property of the program that states what the program does as a whole. Though verification in Argus/V does not guarantee the correctness of the program at one stroke, the more properties of the program proved the closer the program is to what the authors intend. Verification in Argus/V is done using inference rules. Execution in Prolog, on which testing is based, is a special case of the inferences in the verification.",

author = "Tadashi Kanamori and Hiroshi Fujita and Hirohisa Seki and Kenji Horiuchi and Machi Maeji",

year = "1986",

month = dec,

day = "1",

language = "English",

isbn = "0818607432",

publisher = "IEEE",

pages = "994--999",

editor = "Stone, {Harold S.}",

booktitle = "Unknown Host Publication Title",

}

TY - GEN

T1 - ARGUS/V

T2 - A SYSTEM FOR VERIFICATION OF PROLOG PROGRAMS.

AU - Kanamori, Tadashi

AU - Fujita, Hiroshi

AU - Seki, Hirohisa

AU - Horiuchi, Kenji

AU - Maeji, Machi

PY - 1986/12/1

Y1 - 1986/12/1

N2 - The verification system Argus/V for proving properties of Prolog programs is outlined by contrasting verification with testing in logic programming. Specifications in Argus/V are given by a class of first-order formulas, including goals for normal execution. The specification states a partial property of the program that states what the program does as a whole. Though verification in Argus/V does not guarantee the correctness of the program at one stroke, the more properties of the program proved the closer the program is to what the authors intend. Verification in Argus/V is done using inference rules. Execution in Prolog, on which testing is based, is a special case of the inferences in the verification.

AB - The verification system Argus/V for proving properties of Prolog programs is outlined by contrasting verification with testing in logic programming. Specifications in Argus/V are given by a class of first-order formulas, including goals for normal execution. The specification states a partial property of the program that states what the program does as a whole. Though verification in Argus/V does not guarantee the correctness of the program at one stroke, the more properties of the program proved the closer the program is to what the authors intend. Verification in Argus/V is done using inference rules. Execution in Prolog, on which testing is based, is a special case of the inferences in the verification.

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

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

M3 - Conference contribution

AN - SCOPUS:0022882383

SN - 0818607432

SP - 994

EP - 999

BT - Unknown Host Publication Title

A2 - Stone, Harold S.

PB - IEEE

ER -

ARGUS/V: A SYSTEM FOR VERIFICATION OF PROLOG PROGRAMS.

Abstract

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this