package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file TacInduction.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Lang

(* remove parts with n from p into hs accumulator *)
let filter_pred n hs p  =
  F.p_conj @@ List.filter
    (fun p -> if F.occursp n p then (hs := p :: !hs ; false) else true)
    (match F.p_expr p with And ps -> ps | _ -> [p])

(* remove parts with n from step s into hs accumulator *)
let filter_step n hs s =
  match s.Conditions.condition with
  | (Have _ | Type _ | Core _ | Init _ | When _)  ->
    Conditions.map_step (filter_pred n hs) s
  | Probe _ -> s
  | (State _ | Branch _ | Either _) as c ->
    if F.Vars.mem n s.vars then
      (hs := Conditions.pred_cond c :: !hs ; Conditions.step (Have F.p_true))
    else s

let filter_seq n hs seq =
  Conditions.sequence @@ List.map (filter_step n hs) @@ Conditions.list seq

let process value n0 sequent =

  (* Transfrom seq into: hyps => (forall n, goal) *)
  let n = Lang.freshvar ~basename:"n" Qed.Logic.Int in
  let i = Lang.freshvar ~basename:"i" Qed.Logic.Int in
  let vn = F.e_var n in
  let vi = F.e_var i in
  let sigma = Lang.sigma () in
  F.Subst.add sigma value vn ;
  let seq, goal = Conditions.map_sequent (F.p_subst sigma) sequent in
  let hind = ref [] in
  let seq = filter_seq n hind seq in
  let goal_n = F.p_hyps !hind goal in
  let goal_i = F.p_subst_var n vi goal_n in

  (* Base: n = n0 *)
  let goal_base = F.p_imply (F.p_equal vn n0) goal_n in

  (* Hind: n0 <= i < n *)
  let goal_sup =
    let hsup = [ F.p_leq n0 vi ; F.p_lt vi vn ] in
    let hind = F.p_forall [i] (F.p_hyps hsup goal_i) in
    F.p_hyps [F.p_lt n0 vn; hind] goal_n in

  (* Hind: n < i <= n0 *)
  let goal_inf =
    let hinf = [ F.p_lt vn vi ; F.p_leq vi n0 ] in
    let hind = F.p_forall [i] (F.p_hyps hinf goal_i) in
    F.p_hyps [F.p_lt vn n0; hind] goal_n in

  (* All Cases *)
  List.map (fun (name,goal) -> name , (seq,goal)) [
    "Base" , goal_base ;
    "Induction (sup)" , goal_sup ;
    "Induction (inf)" , goal_inf ;
  ]

(* -------------------------------------------------------------------------- *)
(* --- Induction Tactical                                                 --- *)
(* -------------------------------------------------------------------------- *)

let vbase,pbase = Tactical.composer ~id:"base"
    ~title:"Base" ~descr:"Value of base case." ()

class induction =
  object(self)
    inherit Tactical.make
        ~id:"Wp.induction"
        ~title:"Induction"
        ~descr:"Proof by integer induction."
        ~params:[pbase]

    method private get_base () =
      match self#get_field vbase with
      | Tactical.Compose(Code(t, _, _))
      | Inside(_, t) when Lang.F.typeof t = Lang.t_int ->
        Some t
      | Compose(Cint i) ->
        Some (Lang.F.e_bigint i)
      | _ ->
        None

    method select feedback (s : Tactical.selection) =
      begin match self#get_field vbase with
        | Empty ->
          self#set_field vbase (Tactical.int 0) ;
          feedback#update_field vbase
        | _ -> ()
      end ;
      let value = Tactical.selected s in
      if F.is_int value then
        match self#get_base () with
        | Some base -> Tactical.Applicable(process value base)
        | None -> Not_configured
      else Not_applicable

  end

let tactical = Tactical.export (new induction)

(* -------------------------------------------------------------------------- *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct