Skip to content

Draft: Replace axiomatic lists with standard Why3 lists in WP plugin

kwaxer requested to merge kwaxer/frama-c:master into master

This is a follow-up to the discussion from the Frama-C mailing list to bring standard inductive lists to Frama-C WP plugin.

Replaced an axiomatic definition of lists with the standard Why3 one:

  • used standard Why3 list modules;
  • replaced a declared list type with the standard one;
  • provided definitions of all previously specified list functions except for repeat_box;
  • replaced all axioms with lemmas except for those related to repeat_box;
  • proved all new lemmas with Alt-Ergo and Isabelle/HOL;
  • added Why3 session with Why3 realization files and associated Isabelle/HOL theories.

Facts nth_cons and nth_concat received a new premise for the index 0 <= k. All other facts have been kept intact.

Edited by kwaxer

Merge request reports