Changeset 412
 Timestamp:
 Dec 13, 2010, 5:52:18 PM (11 years ago)
 Location:
 Deliverables/D3.1/Report
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Report/report.tex
r408 r412 824 824 extraction is available. 825 825 826 To give a concrete example, the following C program reads an integer 827 using an `external' function and returns its factorial as the 828 program's exit value: 829 \begin{lstlisting}[language=C] 830 int get_input(void); 831 832 int main(void) { 833 int i = get_input(); 834 int r = 1; 835 int j; 836 837 for (j = 2; j<=i; j++) 838 r = r * j; 839 840 return r; 841 } 842 \end{lstlisting} 843 The Clight code is essentially the same, and the \matita{} term is: 844 \begin{lstlisting} 845 ndefinition myprog := mk_program fundef type 846 [mk_pair ?? (succ_pos_of_nat 132 (* get_input *)) 847 (External (succ_pos_of_nat 132) Tnil (Tint I32 Signed)); 848 mk_pair ?? (succ_pos_of_nat 133 (* main *)) (Internal ( 849 mk_function (Tint I32 Signed ) [] [mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed); 850 mk_pair ?? (succ_pos_of_nat 135) (Tint I32 Signed); 851 mk_pair ?? (succ_pos_of_nat 136) (Tint I32 Signed)] 852 (Ssequence 853 (Scall (Some ? (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed))) 854 (Expr (Evar (succ_pos_of_nat 132)) 855 (Tfunction Tnil (Tint I32 Signed))) 856 []) 857 (Ssequence 858 (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed)) 859 (Expr (Econst_int (repr 1)) (Tint I32 Signed))) 860 (Ssequence 861 (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed)) 862 (Expr (Econst_int (repr 2)) (Tint I32 Signed))) 863 (Expr (Ebinop Ole 864 (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed)) 865 (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed))) 866 (Tint I32 Signed )) 867 (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed)) 868 (Expr (Ebinop Oadd 869 (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed)) 870 (Expr (Econst_int (repr 1)) (Tint I32 Signed))) 871 (Tint I32 Signed))) 872 (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed)) 873 (Expr (Ebinop Omul 874 (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed)) 875 (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed))) 876 (Tint I32 Signed))) 877 ) 878 (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 135)) 879 (Tint I32 Signed))))))) 880 ))] 881 (succ_pos_of_nat 133) 882 []. 883 \end{lstlisting} 884 We can use the definitions in the \texttt{Animation.ma} file to reduce 885 the term for a given input (5, in this case): 886 \begin{lstlisting} 887 nremark exec: result ? (exec_up_to myprog 40 [EVint (repr 5)]). 888 nnormalize; (* you can examine the result here *) 889 @; nqed. 890 \end{lstlisting} 891 The result state records the interaction (the \lstinline'EVextcall') 892 and the return result (120 in leastsignificantbit first binary): 893 \begin{lstlisting} 894 result (res (list event$\times$state)) 895 (OK (list event$\times$state) 896 $\langle$[(EVextcall (p1 (p0 (p1 (p0 (p0 (p0 (p0 one))))))) [] 897 (EVint (mk_int (pos (p1 (p0 one))) (inrg_mod (pos (p1 (p0 one)))))))], 898 Returnstate (Vint (mk_int (pos (p0 (p0 (p0 (p1 (p1 (p1 one))))))) 899 (inrg_mod (pos (p0 (p0 (p0 (p1 (p1 (p1 one)))))))))) 900 Kstop MEM $\rangle$) 901 \end{lstlisting} 902 826 903 \appendix 827 904
Note: See TracChangeset
for help on using the changeset viewer.