package frama-c

  1. Overview
  2. Docs

Source file TacChoice.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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Lang
open Conditions
open Tactical

(* -------------------------------------------------------------------------- *)
(* --- Choice Tactical                                                    --- *)
(* -------------------------------------------------------------------------- *)

class choice =
  object
    inherit Tactical.make
        ~id:"Wp.choice"
        ~title:"Choice"
        ~descr:"Select one alternative to be proved."
        ~params:[]

    method select _feedback (s : Tactical.selection) =
      match s with
      | Inside(Goal p,q) ->
        begin
          match F.e_expr p with
          | Qed.Logic.Or qs when List.memq q qs ->
            Applicable (fun (hs,_) -> ["Choice",(hs,F.p_bool q)])
          | _ -> Not_applicable
        end
      | Empty | Compose _ | Clause _ | Inside(Step _,_) | Multi _ ->
        Not_applicable
  end

class absurd =
  object
    inherit Tactical.make
        ~id:"Wp.absurd"
        ~title:"Absurd"
        ~descr:"Contradict the selected clause."
        ~params:[]

    method select _feedback (s : Tactical.selection) =
      match s with
      | Empty | Compose _ | Inside _ | Multi _
        -> Not_applicable
      | Clause(Goal _) ->
        let absurd (seq,goal) =
          let goal = F.p_not goal in
          let step = Conditions.step ~descr:"Absurd" (When goal) in
          let hyps = Conditions.list seq in
          let hyps = Conditions.sequence (hyps @ [step]) in
          [ "Absurd", (hyps , F.p_false) ]
        in Applicable absurd
      | Clause(Step s) ->
        begin
          match s.condition with
          | Have p | When p | Core p | Init p | Type p ->
            let absurd seq =
              let emp = Conditions.(step (Have F.p_true)) in
              let seq = Conditions.replace ~at:s.id emp seq in
              [ "Absurd" , (fst seq , F.p_not p) ]
            in Applicable absurd
          | Branch _ | Either _ | State _ | Probe _ ->
            Not_applicable
        end
  end

class contrapose =
  object
    inherit Tactical.make
        ~id:"Wp.contrapose"
        ~title:"Contrapose"
        ~descr:"Swap hypothesis with conclusion."
        ~params:[]

    method select _feedback (s : Tactical.selection) =
      match s with
      | Empty | Compose _ | Inside _ | Clause(Goal _) | Multi _
        -> Not_applicable
      | Clause(Step s) ->
        begin
          match s.condition with
          | Have p | When p | Core p | Init p | Type p ->
            let contrapose (hs,goal) =
              let descr = "Contrapose the goal." in
              let goal = F.p_not goal in
              let goal = Conditions.(step ~descr (Have goal)) in
              let hs = Conditions.replace ~at:s.id goal (hs , F.p_false) in
              [ "Contrapose" , (fst hs , F.p_not p) ]
            in Applicable contrapose
          | Branch _ | Either _ | State _ | Probe _ ->
            Not_applicable
        end

  end

module Choice =
struct
  let tactical = Tactical.export (new choice)
  let strategy = Strategy.make tactical ~arguments:[]
end

module Absurd =
struct
  let tactical = Tactical.export (new absurd)
  let strategy = Strategy.make tactical ~arguments:[]
end

module Contrapose =
struct
  let tactical = Tactical.export (new contrapose)
  let strategy = Strategy.make tactical ~arguments:[]
end