|
1 {*******************************************************} |
|
2 {FDL Declarations} |
|
3 {Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039} |
|
4 {Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.} |
|
5 {*******************************************************} |
|
6 |
|
7 |
|
8 {DATE : 22-SEP-2011 11:10:50.42} |
|
9 |
|
10 {procedure Loop_Invariant.Proc2} |
|
11 |
|
12 |
|
13 title procedure proc2; |
|
14 |
|
15 function round__(real) : integer; |
|
16 type word32 = integer; |
|
17 const word32__base__first : integer = pending; |
|
18 const word32__base__last : integer = pending; |
|
19 const natural__base__first : integer = pending; |
|
20 const natural__base__last : integer = pending; |
|
21 const integer__base__first : integer = pending; |
|
22 const integer__base__last : integer = pending; |
|
23 const word32__first : integer = pending; |
|
24 const word32__last : integer = pending; |
|
25 const word32__modulus : integer = pending; |
|
26 const word32__size : integer = pending; |
|
27 const natural__first : integer = pending; |
|
28 const natural__last : integer = pending; |
|
29 const natural__size : integer = pending; |
|
30 const integer__first : integer = pending; |
|
31 const integer__last : integer = pending; |
|
32 const integer__size : integer = pending; |
|
33 var a : integer; |
|
34 var b : integer; |
|
35 var c : integer; |
|
36 var loop__1__i : integer; |
|
37 |
|
38 end; |