00001 /* Affiche "hello world" à l'écran */
00002 #include <stdio.h>                /*@\label{lst:hwprep}@*/
00003 
00004 int  main()                       /*@ \label{lst:hwmain} @*/
00005 {
00006         printf("Hello world!\n"); /*@ \label{lst:hwprintf} @*/
00007         return 0;                 /*@ \label{lst:hwret} @*/
00008 }                                 /*@ \label{lst:hwmainend}@*/