*--------------------------------------------------------   
      *   from Frama-C sample
      *   of Fraunhofer Gesellschaft
      *--------------------------------------------------------   
         IDENTIFICATION DIVISION.
         CLASS-ID. Frama.
         ENVIRONMENT DIVISION.
         Configuration Section.
         PROCEDURE DIVISION.
      *--------------------------------------------------------   
      *
      *--------------------------------------------------------   
         IDENTIFICATION DIVISION.
         METHOD-ID. Sum.
         DATA DIVISION.
         Working-Storage Section.
         Linkage Section.
         01 t occurs nt.
           05 pic s9(4)V9(4) comp-4.
         01 n pic s9(4).
         01 s usage is pointer pic s9(4)V9(4) comp-4.
         01 s2 usage is pointer pic s9(4)V9(4) comp-4.
         PROCEDURE DIVISION Using t, n, s, s2.
      *   loop invariant 0<=i<=n     
      *   loop invariant *s ** ysum(0,i-1,t)     
      *   loop invariant *s2 ** mysum(0,i-1,t)     
      *   loop invariant *s2 >= 0.0     
      *   loop assigns *s, *s2     
      *   loop variant n-i     
           perform varying i from 0 until i>n
             add t(i) to s
             compute s2=s2+t(i)*t(i)
           end-perform
         END METHOD Sum.
      *--------------------------------------------------------   
      *
      *--------------------------------------------------------   
         IDENTIFICATION DIVISION.
         METHOD-ID. "Main" .
         DATA DIVISION.
         Working-Storage Section.
         78 n pic s9(4) value 10.
         01 t occurs n.
           05 pic s9(4)V9(4) comp-4.
         01 s pic s9(4)V9(4) comp-4 value 0.0.
         01 s2 usage is pointer pic s9(4)V9(4) comp-4 value 0.0.
         PROCEDURE DIVISION.
           call sum using t, 10, address of s, address of s2
      * assert 0.0 <= s
      * assert 0.0 <= s2
         END METHOD Main.
         END CLASS Frama.
      *--------------------------------------------------------   
      *
      *--------------------------------------------------------   
         PROCEDURE DIVISION.
         IDENTIFICATION DIVISION.
         PROGRAM-ID. OS.
         DATA DIVISION.
         Working-Storage Section.
         Linkage Section.
         PROCEDURE DIVISION.
             invoke Frama
         END Program OS.