0001051: suspicious axiomatization of included,zrange,zunion in .sx file

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001051

Frama-C

Plug-in > wp

public

2011-12-15 18:02

2011-12-16 17:34

Reporter

Jochen

Assigned To

correnson

Priority

normal

Severity

text

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C Nitrogen-20111001

Target Version

Fixed in Version

Summary

0001051: suspicious axiomatization of included,zrange,zunion in .sx file

Description

In the attached proof obligations file "store_fill_function_assigns_po_why.sx" generated by Wp for Simplify, I found some Why axioms looking suspicious. Someone should confirm that their current form is intended. For readability, I transform to Acsl and infix when referring to (sub)formulas.

In axiom "inc_range_range", the conjunct "d<=d+sz" could be simplified to "0<=sz"; similar for "b+sz<0" in axiom "inc_range_empty". In the 1st formula of axiom "inc_union_left" (but not in "inc_union_right"), the "==>" could be sharpened to "<==>". Axiom "inc_sub_zone" could be generalized to "\forall z; (z zunion z) included z". Axiom "inc_permut2" is a consequence of idempotence, associativity, and commutativity of zunion; similar for "union_assoc2"; both axioms look very particular.

Possibly, some above suggestions may cause problems to the provers; e.g. axiomatizing zunion's commutativity probably will. However, some suggestions might yet be useful, I hope.

Tags

No tags attached.

Attached Files

store_fill_function_assigns_po_why.sx [^] (40,900 bytes) 2011-12-15 18:02

store_swap_ranges_exit_assigns_part3_po_why.sx [^] (41,644 bytes) 2011-12-16 17:26

Relationships

Notes
(0002557) Jochen (reporter) 2011-12-16 17:34	The obligation in file "store_swap_ranges_exit_assigns_part3_po_why.sx" cannot be proven by Simplify when any of the axioms "union_sym", "union_assoc", and "inc_sub_zone" is present; all referring to properties of zunion. If all three axioms are commented out, the proof is found in <1sec. (Seemingly, in many cases where code can be verified by Jessie, but not by Wp, obligations concerned with memory locations, zrangs, zunion etc. are involved. Therefor it might be worthwile to think about alternative axiomatizations, or at least to know which axioms cause problems.)

Issue History
Date Modified	Username	Field	Change
2011-12-15 18:02	Jochen	New Issue
2011-12-15 18:02	Jochen	Status	new => assigned
2011-12-15 18:02	Jochen	Assigned To	=> correnson
2011-12-15 18:02	Jochen	File Added: store_fill_function_assigns_po_why.sx
2011-12-16 17:26	Jochen	File Added: store_swap_ranges_exit_assigns_part3_po_why.sx
2011-12-16 17:34	Jochen	Note Added: 0002557