東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Mapping Programs to Equations.

Mohammadi, Hessamaldin.

Linked to FindBook

Google Book

Amazon

博客來

Mapping Programs to Equations.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Mapping Programs to Equations./
Author:	Mohammadi, Hessamaldin.
Published:	Ann Arbor : ProQuest Dissertations & Theses, : 2023,
Description:	128 p.
Notes:	Source: Dissertations Abstracts International, Volume: 85-04, Section: B.
Contained By:	Dissertations Abstracts International85-04B.
Subject:	Computer science. -
Online resource:	https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30310138
ISBN:	9798380604987

Mapping Programs to Equations.
Mohammadi, Hessamaldin.

Mapping Programs to Equations. - Ann Arbor : ProQuest Dissertations & Theses, 2023 - 128 p.

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

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

This item must not be sold to any third party vendors.

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.

ISBN: 9798380604987Subjects--Topical Terms:

523869
Computer science.
Subjects--Index Terms:

Equations

Mapping Programs to Equations.
LDR:03319nmm a2200397 4500 001 2395630
005 20240517104936.5
006 m o d
007 cr#unu||||||||
008 251215s2023 ||||||||||||||||| ||eng d
020 $a 9798380604987
035 $a (MiAaPQ)AAI30310138
035 $a AAI30310138
040 $a MiAaPQ $c MiAaPQ
100 1 $a Mohammadi, Hessamaldin. $3 3765140
245 1 0 $a Mapping Programs to Equations.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2023
300 $a 128 p.
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.
506 $a This item must not be sold to any third party vendors.
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.
590 $a School code: 0152.
650 4 $a Computer science. $3 523869
650 4 $a Theoretical mathematics. $3 3173530
650 4 $a Information technology. $3 532993
653 $a Equations
653 $a Software engineering
653 $a Static analysis
653 $a Test
653 $a Verification
690 $a 0984
690 $a 0642
690 $a 0489
710 2 $a New Jersey Institute of Technology. $b Department of Computer Science. $3 3544036
773 0 $t Dissertations Abstracts International $g 85-04B.
790 $a 0152
791 $a Ph.D.
792 $a 2023
793 $a English
856 4 0 $u https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30310138