Thumbnail
Access Restriction
Subscribed

Author Wegbreit, Ben
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1976
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract It is shown that specifications of program performance can be formally verified. Formal verification techniques, in particular, the method of inductive assertions, can be adapted to show that a program's maximum or mean execution time is correctly described by specifications supplied with the program. To formally establish the mean execution time, branching probabilities are expressed using inductive assertions which involve probability distributions. Verification conditions are formed and proved which establish that if the input distribution is correctly described by the input specifications, then the inductive assertions correctly describe the probability distributions of the data during execution. Once the inductive assertions are shown to be correct, branching probabilities are obtained and mean computation time is computed.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1976-10-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 23
Issue Number 4
Page Count 9
Starting Page 691
Ending Page 699


Open content in new tab

   Open content in new tab
Source: ACM Digital Library