Quellsprache: Binärcode.siv aufgebrochen in jeweils 16 ZeichenBAT {BAT[164] Abap[250] [0]}zum Wurzelverzeichnis wechseln
*****************************************************************************
Semantic Analysis of SPARK Text
Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
*****************************************************************************
CREATED 29-NOV-2010, 14:30:17 SIMPLIFIED 29-NOV-2010, 14:30:18
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
function Sqrt.Isqrt
For path(s) from start to run-time check associated with statement of line 7:
function_isqrt_1.
*** true . /* all conclusions proved */
For path(s) from start to assertion of line 9:
function_isqrt_2.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to assertion of line 9:
function_isqrt_3.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to run-time check associated with
statement of line 10:
function_isqrt_4.
H1: r * r <= n .
H2: n >= 0 .
H3: n <= 2147483647 .
H4: r >= 0 .
H5: r <= 2147483647 .
H6: integer__size >= 0 .
H7: natural__size >= 0 .
->
C1: 2 * r <= 2147483646 .
C2: 2 * r <= 2147483647 .
For path(s) from assertion of line 9 to run-time check associated with
statement of line 11:
function_isqrt_5.
*** true . /* all conclusions proved */
For path(s) from assertion of line 9 to finish:
function_isqrt_6.
*** true . /* all conclusions proved */
[ zur Elbe Produktseite wechseln0.109Quellennavigators
]
