isabelle: src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c

41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	1	/*********************************************************/
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	2	/Proof Rule Declarations/
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	3	/Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039/
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	4	/Copyright (C) 2010 Altran Praxis Limited, Bath, U.K./
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	5	/*********************************************************/
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	6
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	7
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	8	/DATE : 29-NOV-2010 14:30:10.98/
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	9
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	10	/procedure Greatest_Common_Divisor.G_C_D/
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	11
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	12
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	13	rule_family g_c_d_rules:
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	14	X requires [X:any] &
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	15	X <= Y requires [X:ire, Y:ire] &
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	16	X >= Y requires [X:ire, Y:ire].
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	17
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	18	g_c_d_rules(1): integer__size >= 0 may_be_deduced.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	19	g_c_d_rules(2): integer__first may_be_replaced_by -2147483648.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	20	g_c_d_rules(3): integer__last may_be_replaced_by 2147483647.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	21	g_c_d_rules(4): integer__base__first may_be_replaced_by -2147483648.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	22	g_c_d_rules(5): integer__base__last may_be_replaced_by 2147483647.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	23	g_c_d_rules(6): natural__size >= 0 may_be_deduced.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	24	g_c_d_rules(7): natural__first may_be_replaced_by 0.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	25	g_c_d_rules(8): natural__last may_be_replaced_by 2147483647.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	26	g_c_d_rules(9): natural__base__first may_be_replaced_by -2147483648.
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	27	g_c_d_rules(10): natural__base__last may_be_replaced_by 2147483647.

author	haftmann
	Sun, 21 Apr 2013 10:41:18 +0200
changeset 51724	80f9906ede19
parent 41561	d1318f3c86ba
permissions	-rw-r--r--