Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
frama-sample.cob
Sprache: Unknown
|
*--------------------------------------------------------
* 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.
[ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
]
|
|
