A Correct-by-Construction Checker for Constraints on a Railway-Oriented Databases

A Correct-by-Construction Checker for Constraints on a Railway-Oriented Databases. The design is detailed in the research report Design of a correct-by-construction checker for constraints on railway-oriented databases. Below in the ZIP archive we provide the code and the proof sessions that allow replaying the proofs, a Makefile that allow to build the executable, and some test files. We also give the HTML report of the proof sessions.

Authors: Claude Marché / Matteo Manighetti / Noé Canva

Topics: Inductive predicates / Semantics of languages / Graph Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

Why3 Proof Results for Project "graph_traversal"

Theory "graph_traversal.Graph": fully verified

Obligations		Alt-Ergo 2.6.2	CVC4 1.8	CVC5 1.2.0	Z3 4.12.2	Z3 4.12.2 (noBV)	Z3 4.13.2
VC for graph		---	---	0.03	---	---	---
VC for path_avoiding_non_cyclic		---	---	---	---	---	---
split_vc
	unreachable point	---	---	0.03	---	---	---
	variant decrease	0.03	---	---	---	---	---
	precondition	---	---	0.03	---	---	---
	precondition	---	---	0.07	---	---	---
	postcondition	0.05	---	---	---	---	---
VC for path_avoiding_monotone		---	---	---	---	---	---
split_vc
	variant decrease	---	---	0.02	---	---	---
	precondition	---	0.18	---	---	---	---
	precondition	0.04	---	---	---	---	---
	postcondition	0.18	---	---	---	---	---
VC for path_avoiding_split		---	---	---	---	---	---
split_vc
	unreachable point	---	---	0.15	---	---	---
	assertion	---	---	0.07	---	---	---
	assertion	---	---	0.82	---	---	---
	unreachable point	---	0.11	---	---	---	---
	assertion	---	0.20	---	---	---	---
	variant decrease	---	---	0.04	---	---	---
	precondition	---	---	0.21	---	---	---
	precondition	0.03	---	---	---	---	---
	precondition	---	---	---	0.05	---	---
	precondition	---	---	0.20	---	---	---
	postcondition	---	---	0.54	---	---	---
VC for dfs		---	---	---	---	---	---
split_vc
	precondition	---	---	---	---	0.02	---
	variant decrease	---	---	---	0.06	---	---
	precondition	0.02	---	---	---	---	---
	precondition	---	---	0.18	---	---	---
	precondition	0.05	---	---	---	---	---
	precondition	0.05	---	---	---	---	---
	precondition	0.05	---	---	---	---	---
	precondition	---	---	0.05	---	---	---
	precondition	---	---	0.03	---	---	---
	postcondition	---	---	0.13	---	---	---
	postcondition	---	---	0.18	---	---	---
VC for dfs_list		---	---	---	---	---	---
split_vc
	variant decrease	---	---	0.07	---	---	---
	precondition	---	---	0.09	---	---	---
	precondition	---	---	---	---	---	0.01
	precondition	---	0.06	---	---	---	---
	variant decrease	0.03	---	---	---	---	---
	precondition	---	---	0.05	---	---	---
	precondition	---	0.12	---	---	---	---
	precondition	---	---	0.06	---	---	---
	precondition	0.05	---	---	---	---	---
	precondition	---	---	0.83	---	---	---
	precondition	0.04	---	---	---	---	---
	precondition	---	---	---	0.02	---	---
	postcondition	0.03	---	---	---	---	---
	postcondition	---	---	0.70	---	---	---
VC for exists_path_avoiding		---	---	---	---	---	---
split_vc
	precondition	---	0.06	---	---	---	---
	precondition	---	---	---	---	---	0.01
	precondition	---	---	---	---	0.01	---
	postcondition	---	---	0.05	---	---	---

Why3 Proof Results for Project "db_engine"

Theory "db_engine.Db_engine_types": fully verified

Obligations	Alt-Ergo 2.6.2	CVC5 1.2.0
VC for table	0.08	---
VC for empty_table	---	0.07

Theory "db_engine.Db_engine": fully verified

Obligations					Alt-Ergo 2.6.2	CVC4 1.8	CVC5 1.2.0	Z3 4.12.2
VC for list_nth					---	---	---	---
split_vc
	exceptional postcondition				---	---	---	0.02
	postcondition				0.04	---	---	---
	integer overflow				0.05	---	---	---
	variant decrease				---	---	0.03	---
	postcondition				---	---	0.10	---
	exceptional postcondition				---	---	0.03	---
	exceptional postcondition				0.03	---	0.10	---
VC for list_nth_functional					0.05	---	0.11	---
VC for get_record					1.69	---	---	---
VC for get_id					0.07	---	0.05	---
VC for read_field_names					0.11	---	0.64	---
VC for chop_extra_lines					---	---	0.07	---
VC for read_lines					---	---	---	---
split_vc
	precondition				0.07	---	0.18	---
	exceptional postcondition				0.03	---	---	---
	exceptional postcondition				---	---	0.03	---
	variant decrease				0.05	---	0.15	---
	precondition				---	---	0.05	---
	precondition				---	---	0.03	---
	precondition				---	---	---	---
	split_vc
		precondition			---	---	---	---
		inline_goal
			precondition		---	---	---	---
			split_all_full
				precondition	---	---	0.24	---
				precondition	0.05	---	---	---
				precondition	---	---	0.16	---
				precondition	0.12	---	---	---
	postcondition				---	---	0.05	---
	exceptional postcondition				---	---	0.03	---
	exceptional postcondition				0.06	---	0.04	---
	exceptional postcondition				---	---	0.14	---
	exceptional postcondition				0.03	---	0.02	---
	exceptional postcondition				---	---	0.03	---
	exceptional postcondition				---	---	0.03	---
	exceptional postcondition				---	---	0.03	---
	postcondition				---	---	0.14	---
VC for read_table					---	---	---	---
split_vc
	exceptional postcondition				---	---	0.03	---
	integer overflow				---	---	0.06	---
	unreachable point				0.04	---	0.03	---
	precondition				---	---	0.04	0.02
	precondition				---	---	0.14	---
	precondition				0.10	---	---	---
	precondition				0.04	---	---	---
	exceptional postcondition				0.05	---	0.15	---
	exceptional postcondition				---	---	0.14	---
	exceptional postcondition				---	---	0.03	---
	exceptional postcondition				---	---	0.14	0.01
	exceptional postcondition				---	---	0.02	---
VC for add_table					---	---	0.11	---
VC for add_fun_env					---	---	0.04	---
VC for eval_expr					---	---	---	---
split_vc
	postcondition				0.05	---	---	---
	postcondition				---	---	0.12	---
	postcondition				0.13	---	---	---
	postcondition				0.07	---	---	---
	exceptional postcondition				0.04	---	---	---
	loop invariant init				0.08	---	---	---
	loop variant decrease				---	---	---	0.13
	loop invariant preservation				---	---	0.11	---
	postcondition				0.07	---	---	---
	exceptional postcondition				0.05	---	---	---
	postcondition				---	---	0.63	---
	exceptional postcondition				---	---	0.10	---
	postcondition				---	---	0.73	---
	exceptional postcondition				---	---	0.06	---
	postcondition				---	---	0.68	---
	exceptional postcondition				0.04	---	---	---
	postcondition				---	---	0.50	---
	exceptional postcondition				---	---	0.10	---
	exceptional postcondition				---	---	0.09	---
	exceptional postcondition				---	---	---	0.07
	exceptional postcondition				0.12	---	---	---
	exceptional postcondition				---	---	0.14	---
	exceptional postcondition				0.13	---	---	---
	exceptional postcondition				0.03	---	---	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				---	---	0.06	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				0.05	---	---	---
	postcondition				0.06	---	---	---
	postcondition				0.05	---	0.18	---
	postcondition				---	---	0.21	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				---	---	0.04	---
	exceptional postcondition				0.05	---	---	---
	exceptional postcondition				---	---	0.16	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				0.15	---	0.04	---
	exceptional postcondition				---	---	0.08	---
	exceptional postcondition				---	---	0.07	---
	exceptional postcondition				---	---	0.08	---
	exceptional postcondition				---	---	0.07	---
	exceptional postcondition				---	---	0.04	---
	exceptional postcondition				---	---	0.04	---
	postcondition				---	---	0.20	---
	postcondition				0.09	---	---	---
	postcondition				0.07	---	---	---
	exceptional postcondition				0.06	---	---	---
	exceptional postcondition				---	---	0.06	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				---	---	0.07	---
	exceptional postcondition				---	---	0.04	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				0.03	---	---	---
	exceptional postcondition				0.05	---	---	---
	exceptional postcondition				0.05	---	---	---
	exceptional postcondition				0.15	---	0.05	---
	exceptional postcondition				---	---	0.04	---
	postcondition				0.14	---	---	---
	exceptional postcondition				0.14	---	0.06	---
	exceptional postcondition				0.08	---	---	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				---	---	0.05	---
	exceptional postcondition				---	---	0.04	---
exceptional postcondition				0.06	---	---	---
exceptional postcondition				0.04	---	---	---
postcondition				---	---	0.10	---
exceptional postcondition				0.14	---	0.05	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				0.04	---	0.06	---
postcondition				---	---	0.10	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				0.04	---	---	---
exceptional postcondition				0.03	---	---	---
exceptional postcondition				0.04	---	---	---
exceptional postcondition				0.03	---	0.05	---
exceptional postcondition				---	---	0.03	---
postcondition				---	---	0.14	---
exceptional postcondition				0.04	---	0.08	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.04	---
exceptional postcondition				---	---	0.05	---
postcondition				0.06	---	---	---
exceptional postcondition				0.04	---	---	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				0.03	---	0.05	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.04	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				0.03	---	0.06	---
exceptional postcondition				0.05	---	---	---
exceptional postcondition				---	---	0.03	---
exceptional postcondition				---	---	0.04	---
postcondition				0.07	---	---	---
exceptional postcondition				0.06	---	---	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.16	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.07	---
exceptional postcondition				---	---	0.07	---
exceptional postcondition				0.04	---	---	---
exceptional postcondition				---	---	0.08	---
exceptional postcondition				---	---	0.09	---
exceptional postcondition				---	---	0.06	---
loop invariant init				0.10	---	---	---
loop invariant init				0.05	---	---	---
postcondition				0.06	---	---	---
loop variant decrease				0.07	---	---	---
loop invariant preservation				1.28	---	---	---
loop invariant preservation				0.07	---	---	---
loop variant decrease				0.07	---	---	---
loop invariant preservation				0.88	---	---	---
loop invariant preservation				---	---	0.24	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				0.05	---	---	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.07	---
postcondition				0.06	---	---	---
exceptional postcondition				0.09	---	---	---
exceptional postcondition				---	---	0.07	---
exceptional postcondition				0.05	---	---	---
exceptional postcondition				0.04	---	---	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.05	---
postcondition				---	---	0.08	---
exceptional postcondition				0.15	---	0.05	---
exceptional postcondition				0.04	---	0.07	---
exceptional postcondition				---	---	0.04	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.06	---
loop invariant init				0.11	---	---	---
loop invariant init				0.09	---	---	---
loop variant decrease				---	---	---	---
split_vc
	loop variant decrease			0.07	---	---	---
	loop variant decrease			0.06	---	---	---
loop invariant preservation				---	---	---	---
inline_goal
	loop invariant preservation			---	---	---	---
	split_vc
		loop invariant preservation		0.08	---	---	---
		loop invariant preservation		---	---	0.52	---
		loop invariant preservation		0.15	---	---	---
loop invariant preservation				0.07	---	---	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				0.04	---	---	---
exceptional postcondition				---	---	0.04	---
exceptional postcondition				---	---	0.04	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				---	---	0.06	---
loop variant decrease				---	---	---	---
split_vc
	loop variant decrease			0.08	---	---	---
	loop variant decrease			0.10	---	---	---
loop invariant preservation				---	---	---	---
inline_goal
	loop invariant preservation			---	---	---	---
	split_all_full
		VC for eval_expr		---	---	0.18	---
		VC for eval_expr		---	---	---	---
		split_vc
			VC for eval_expr	---	0.95	---	---
		VC for eval_expr		---	---	0.36	---
loop invariant preservation				0.09	---	---	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.07	---
exceptional postcondition				0.06	---	0.16	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.06	---
postcondition				---	---	0.12	---
exceptional postcondition				---	---	0.10	---
exceptional postcondition				---	---	0.06	---
exceptional postcondition				0.05	---	---	---
exceptional postcondition				0.07	---	0.07	---
exceptional postcondition				---	---	0.14	---
exceptional postcondition				0.12	---	---	---
postcondition				---	---	0.12	---
exceptional postcondition				0.04	---	0.06	---
exceptional postcondition				---	---	0.05	---
exceptional postcondition				---	---	0.09	---
exceptional postcondition				0.04	---	---	---
exceptional postcondition				---	---	---	0.04
VC for eval_expr_list					---	---	---	---
split_vc
	postcondition				0.04	---	---	---
	postcondition				0.05	---	---	---
	exceptional postcondition				---	---	0.04	---
	exceptional postcondition				---	---	0.07	---
	exceptional postcondition				---	---	0.07	---
	exceptional postcondition				---	---	0.16	---
	exceptional postcondition				0.05	---	---	---
	exceptional postcondition				0.06	---	---	---
	exceptional postcondition				0.05	---	---	---
	exceptional postcondition				---	---	0.04	---
	exceptional postcondition				---	---	0.04	---
	exceptional postcondition				0.03	---	---	---
VC for empty_env					---	---	0.08	---
VC for check_main					---	---	---	---
split_vc
	exceptional postcondition				---	---	0.07	---
	postcondition				0.06	---	---	---
	exceptional postcondition				0.04	---	---	---
	exceptional postcondition				0.04	---	---	---
	exceptional postcondition				0.06	---	---	---
	exceptional postcondition				0.03	---	0.09	---
	exceptional postcondition				---	---	0.04	---
	exceptional postcondition				---	---	0.03	---
VC for optim_conj					---	---	---	---
split_vc
	postcondition				---	---	---	---
	split_vc
		postcondition			2.60	---	---	---
		postcondition			0.41	---	---	---
		postcondition			---	---	0.93	---
		postcondition			---	---	0.43	---
		postcondition			---	---	0.12	---

Theory "db_engine.Db_with_predefined": fully verified

Obligations		Alt-Ergo 2.6.2	CVC5 1.2.0	Z3 4.12.2	Z3 4.13.2
VC for twolayer_graph		0.08	---	---	---
VC for empty_graph		0.07	---	---	---
VC for eval_context		0.05	---	---	---
VC for try_find		---	0.03	---	---
VC for try_find_ident		---	0.06	---	---
VC for compute_next		---	---	---	---
split_vc
	postcondition	0.69	---	---	---
	postcondition	0.41	---	---	---
	postcondition	0.19	---	---	---
	exceptional postcondition	0.05	---	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	0.05	---	---	---
	exceptional postcondition	0.05	---	---	---
	postcondition	0.54	---	---	---
	postcondition	0.13	---	---	---
	postcondition	0.08	---	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	0.04	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	---	0.03	---
	exceptional postcondition	---	0.06	---	---
	postcondition	0.42	---	---	---
	postcondition	---	0.40	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	0.05	---	---	---
	postcondition	---	0.11	---	---
	postcondition	0.06	---	---	---
	postcondition	---	0.13	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	0.06	---	---
VC for compute_prev		---	---	---	---
split_vc
	postcondition	0.95	---	---	---
	postcondition	0.37	---	---	---
	postcondition	0.16	---	---	---
	exceptional postcondition	0.03	---	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	---	0.04	---
	exceptional postcondition	0.06	---	---	---
	postcondition	0.49	---	---	---
	postcondition	0.20	---	---	---
	postcondition	0.16	---	---	---
	exceptional postcondition	---	0.08	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	0.08	---	---
	exceptional postcondition	0.05	---	---	---
	postcondition	0.31	---	---	---
	postcondition	---	0.47	---	---
	postcondition	0.07	---	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	---	0.04	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	0.07	---	---
	postcondition	0.04	---	---	---
	postcondition	0.07	---	---	---
	postcondition	---	0.10	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	---	0.03	---
VC for create_graph		---	---	---	---
split_vc
	loop invariant init	0.04	---	---	---
	loop invariant init	0.07	---	---	---
	loop invariant init	0.04	---	---	---
	loop invariant init	---	0.11	---	---
	loop invariant init	0.05	---	---	---
	loop invariant init	0.05	---	---	---
	loop invariant init	0.07	---	---	---
	loop invariant init	---	0.21	---	---
	loop variant decrease	---	0.25	---	---
	loop invariant preservation	0.06	---	---	---
	loop invariant preservation	0.05	---	---	---
	loop invariant preservation	0.05	---	---	---
	loop invariant preservation	0.15	---	---	---
	loop invariant preservation	0.09	---	---	---
	loop invariant preservation	0.15	---	---	---
	loop invariant preservation	0.05	---	---	---
	loop invariant preservation	2.15	---	---	---
	loop invariant init	0.07	---	---	---
	loop invariant init	0.03	---	---	---
	loop invariant init	0.05	---	---	---
	loop invariant init	0.11	---	---	---
	loop invariant init	0.05	---	---	---
	assertion	---	0.26	---	---
	precondition	0.08	---	---	---
	precondition	0.05	---	---	---
	precondition	---	0.05	---	---
	precondition	0.13	---	---	---
	precondition	0.06	---	---	---
	precondition	0.04	---	---	---
	assertion	0.04	---	---	---
	precondition	0.04	---	---	---
	precondition	0.06	---	---	---
	precondition	---	0.10	---	---
	precondition	0.03	---	---	---
	precondition	---	0.41	---	---
	precondition	---	0.10	---	---
	assertion	---	0.14	---	---
	loop variant decrease	0.06	---	---	---
	loop invariant preservation	0.14	---	---	---
	loop invariant preservation	---	0.08	---	---
	loop invariant preservation	---	0.66	---	---
	loop invariant preservation	0.23	---	---	---
	loop invariant preservation	---	1.40	---	---
	exceptional postcondition	---	0.06	---	---
	exceptional postcondition	0.06	---	---	---
	exceptional postcondition	---	0.06	---	---
	assertion	---	0.38	---	---
	precondition	0.08	---	---	---
	precondition	---	0.08	---	---
	postcondition	---	0.28	---	---
	exceptional postcondition	0.05	---	---	---
VC for try_find_predefined		---	0.04	---	---
VC for vertex_of		---	---	---	---
split_vc
	postcondition	0.06	---	---	---
	postcondition	0.05	---	---	---
	exceptional postcondition	---	---	---	0.03
VC for vertex_set_of		---	---	---	---
split_vc
	loop invariant init	0.05	---	---	---
	loop invariant init	0.05	---	---	---
	loop invariant init	0.06	---	---	---
	loop variant decrease	0.07	---	---	---
	loop invariant preservation	0.19	---	---	---
	loop invariant preservation	0.08	---	---	---
	loop invariant preservation	0.11	---	---	---
	exceptional postcondition	0.05	---	---	---
	postcondition	0.04	---	---	---
	postcondition	0.08	---	---	---
VC for check_exists_path_avoiding		---	---	---	---
split_vc
	precondition	---	0.06	---	---
	precondition	0.04	---	---	---
	precondition	0.04	---	---	---
	postcondition	0.09	---	---	---
	exceptional postcondition	0.06	---	---	---
	exceptional postcondition	0.05	---	---	---
	exceptional postcondition	0.05	---	---	---
VC for eval_predefined		---	---	---	---
split_vc
	postcondition	0.06	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	0.06	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	0.04	---	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	postcondition	0.13	---	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	0.07	---	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	---	---	0.01	---
	postcondition	0.07	---	---	---
	exceptional postcondition	0.04	---	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	---	0.07	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	---	0.06	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	---	0.05	---	---
	postcondition	---	0.11	---	---
	variant decrease	---	0.06	---	---
	postcondition	---	0.22	---	---
	exceptional postcondition	0.05	---	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	0.05	---	---	---
	postcondition	0.06	---	---	---
	exceptional postcondition	---	0.09	---	---
	exceptional postcondition	---	0.05	---	---
	precondition	---	0.06	---	---
	postcondition	0.19	---	---	---
	exceptional postcondition	0.05	---	---	---
	exceptional postcondition	---	0.05	---	---
	exceptional postcondition	0.04	---	---	---
	exceptional postcondition	---	0.06	---	---
	exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	---	0.01	---
exceptional postcondition	---	---	0.01	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
postcondition	0.08	---	---	---
exceptional postcondition	---	0.06	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.06	---	---
exceptional postcondition	---	0.05	---	---
postcondition	0.06	---	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	0.04	---	---	---
exceptional postcondition	0.04	---	---	---
postcondition	0.06	---	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	0.04	---	---	---
postcondition	0.06	---	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.06	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
exceptional postcondition	---	0.05	---	---
VC for eval_predefined'refn		0.03	0.05	---	---

Toccata

Formally Verified Programs, Certified Tools and Numerical Computations