國立虎尾科技大學 |

Mapping Programs to Equations.

紀錄類型:	書目-語言資料,手稿 : Monograph/item
正題名/作者:	Mapping Programs to Equations./
作者:	Mohammadi, Hessamaldin.
面頁冊數:	1 online resource (128 pages)
附註:	Source: Dissertations Abstracts International, Volume: 85-04, Section: B.
Contained By:	Dissertations Abstracts International85-04B.
標題:	Computer science. -
電子資源:	click for full text (PQDT)
ISBN:	9798380604987

Mapping Programs to Equations.
Mohammadi, Hessamaldin.

Mapping Programs to Equations. - 1 online resource (128 pages)

Source: Dissertations Abstracts International, Volume: 85-04, Section: B.

Thesis (Ph.D.)--New Jersey Institute of Technology, 2023.

Includes bibliographical references

Extracting the function of a program from a static analysis of its source code is a valuable capability in software engineering; at a time when there is increasing talk of using AI (Artificial Intelligence) to generate software from natural language specifications, it becomes increasingly important to determine the exact function of software as written, to figure out what AI has understood the natural language specification to mean. For all its criticality, the ability to derive the domain-to-range function of a program has proved to be an elusive goal, due primarily to the difficulty of deriving the function of iterative statements. Several automated tools obviate this difficulty by unrolling the loops; but this is clearly an imperfect solution, especially in light of the fact that loops capture most of the computing power of a program, are the locus of most of its complexity, and the source of most of its faults. This dissertation investigates a three-step process to map a program written in a C-like language into a function from inputs to outputs, or from initial states to final states. The semantics of iterative statements are captured (while loops, repeat loops, for loops), including nested iterative statements, by means of the concept of invariant relation; an invariant relation is a reflexive transitive relation that links program states separated by an arbitrary number of iterations.But the function derived for large and complex programs may be too unwieldy to be useful, not unlike drinking from a fire hose. In order to enable the user to query the program at scale, four functions are proposed. We propose four functions: Assume(), which enables the user to make assumptions about program states or program parts; Capture(), which enables the user to capture the state of the program at some label of the function of some program part; Verify(), which enables the user to verify a unary assertion about the state of the program at some label, or a binary assertion about a program part; and Establish(), which is envisioned to use program repair techniques to modify the program so as to make a Verify() query return true.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2024

Mode of access: World Wide Web

ISBN: 9798380604987Subjects--Topical Terms:

573171
Computer science.
Subjects--Index Terms:

EquationsIndex Terms--Genre/Form:

554714
Electronic books.

Mapping Programs to Equations.
LDR:03472ntm a22003977 4500 001 1143726
005 20240517104936.5
006 m o d
007 cr mn ---uuuuu
008 250605s2023 xx obm 000 0 eng d
020 $a 9798380604987
035 $a (MiAaPQ)AAI30310138
035 $a AAI30310138
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Mohammadi, Hessamaldin. $3 1468506
245 1 0 $a Mapping Programs to Equations.
264 0 $c 2023
300 $a 1 online resource (128 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertations Abstracts International, Volume: 85-04, Section: B.
500 $a Advisor: Mili, Ali.
502 $a Thesis (Ph.D.)--New Jersey Institute of Technology, 2023.
504 $a Includes bibliographical references
520 $a Extracting the function of a program from a static analysis of its source code is a valuable capability in software engineering; at a time when there is increasing talk of using AI (Artificial Intelligence) to generate software from natural language specifications, it becomes increasingly important to determine the exact function of software as written, to figure out what AI has understood the natural language specification to mean. For all its criticality, the ability to derive the domain-to-range function of a program has proved to be an elusive goal, due primarily to the difficulty of deriving the function of iterative statements. Several automated tools obviate this difficulty by unrolling the loops; but this is clearly an imperfect solution, especially in light of the fact that loops capture most of the computing power of a program, are the locus of most of its complexity, and the source of most of its faults. This dissertation investigates a three-step process to map a program written in a C-like language into a function from inputs to outputs, or from initial states to final states. The semantics of iterative statements are captured (while loops, repeat loops, for loops), including nested iterative statements, by means of the concept of invariant relation; an invariant relation is a reflexive transitive relation that links program states separated by an arbitrary number of iterations.But the function derived for large and complex programs may be too unwieldy to be useful, not unlike drinking from a fire hose. In order to enable the user to query the program at scale, four functions are proposed. We propose four functions: Assume(), which enables the user to make assumptions about program states or program parts; Capture(), which enables the user to capture the state of the program at some label of the function of some program part; Verify(), which enables the user to verify a unary assertion about the state of the program at some label, or a binary assertion about a program part; and Establish(), which is envisioned to use program repair techniques to modify the program so as to make a Verify() query return true.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2024
538 $a Mode of access: World Wide Web
650 4 $a Computer science. $3 573171
650 4 $a Theoretical mathematics. $3 1180455
650 4 $a Information technology. $3 559429
653 $a Equations
653 $a Software engineering
653 $a Static analysis
653 $a Test
653 $a Verification
655 7 $a Electronic books. $2 local $3 554714
690 $a 0984
690 $a 0642
690 $a 0489
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a New Jersey Institute of Technology. $b Department of Computer Science. $3 1468489
773 0 $t Dissertations Abstracts International $g 85-04B.
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30310138 $z click for full text (PQDT)