Download Symbolic Execution Tool User Manual

Symbolic Execution Tool User Manual
This symbolic execution tool was developed under Microsoft windows XP and Maple 9.5.
You can use examples.mpl to try our Symbolic Execution Tool. There are two ways to
use our examples file. One way is to test the examples and modules in batch input and the
other way is to test the examples and the modules Interactively
Method 1: Test the Examples and the Modules In Batch Input
To run test, please type the following command:
restart;
read “C:\\symbolic execution tool\\Examples.mpl”;
infolevel[myname]:=2;
Figure 1: Shows the command to read the examples.mpl file
Figure 2: Shows the result from figure1 command.
All the example result file can also be download from the examplesresult.mw
Method 2: Test the Examples and the Modules Interactively.
Open the example.mpl file and copy three lines showing in figure 3 into the Maple work
sheet.
To run main module, please type the following command:
restart;
read “C:\\symbolic execution tool\\mainmodule.mpl”;
infolevel[myname]:=2;
Figure 3: Shows the Command to Read the mainmodule.mpl File
Figure 4: Show the Result from Figure 3 Command
To run factorial function, please type the followings:
ff:=proc(n)
local j, fac;
j:=1;
fac:=1;
while j<>n do
j:=j+1;
fac:=fac*j;
end do;
fac;
end proc:
e5:=GEN:-gen_eqns(ff);
Figure 5: Shows Inputing the Test Function and Call the gen_eqns Function in GEN
Module to Generate Relations.
Note: The input parameter value for the gen_eqns is the name of the test function.
To call solve function, please type the following:
SOLVE:-solve1(e5);
Figure 6: Shows Calling the solve1 Funtion in SOLVE Module to Generate Initial
Functions, Recursive Functions and Symbolic Result.
You can test other functions provided in the examples.mpl in the above method.
Comments: For the input program which can be solved by our symbolic computation tool,
please reference Yun Zhai’s Master thesis chapter 5 (System Analysis).
Also, it is not recommend using the Maple key word as the variable for the input
program.