Changeset 412 for Deliverables/D3.1


Ignore:
Timestamp:
Dec 13, 2010, 5:52:18 PM (9 years ago)
Author:
campbell
Message:

Add example of animation.

Location:
Deliverables/D3.1/Report
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/Report/report.tex

    r408 r412  
    824824extraction is available.
    825825
     826To give a concrete example, the following C program reads an integer
     827using an `external' function and returns its factorial as the
     828program's exit value:
     829\begin{lstlisting}[language=C]
     830int get_input(void);
     831
     832int 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}
     843The Clight code is essentially the same, and the \matita{} term is:
     844\begin{lstlisting}
     845ndefinition 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}
     884We can use the definitions in the \texttt{Animation.ma} file to reduce
     885the term for a given input (5, in this case):
     886\begin{lstlisting}
     887nremark exec: result ? (exec_up_to myprog 40 [EVint (repr 5)]).
     888nnormalize;  (* you can examine the result here *)
     889@; nqed.
     890\end{lstlisting}
     891The result state records the interaction (the \lstinline'EVextcall')
     892and the return result (120 in least-significant-bit first binary):
     893\begin{lstlisting}
     894result (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
    826903\appendix
    827904
Note: See TracChangeset for help on using the changeset viewer.