Module: ADSL::Verification::FormulaGenerators

Includes:
Parser, Utils
Included in:
Extract::Rails::InvariantExtractor, Parser::ASTNode, FormulaBuilder, VerificationCase, FalseClass, TrueClass
Defined in:
lib/adsl/verification/formula_generators.rb

Instance Method Summary collapse

Methods included from Utils

#classname_for_classname, #infer_classname_from_varname, #t

Instance Method Details

#[](formula) ⇒ Object 



96
97
98
99
100
101
 
# File 'lib/adsl/verification/formula_generators.rb', line 96

def [](formula)
  in_formula_builder do |fb|
    formula = formula.adsl_ast if formula.respond_to? :adsl_ast
    fb.adsl_stack << formula
  end
end

#and(*params) ⇒ Object 



130
131
132
 
# File 'lib/adsl/verification/formula_generators.rb', line 130

def and(*params)
  binary_op_with_any_number_of_params :and, ASTAnd, params
end

#binary_op(op, klass, params) ⇒ Object 



116
117
118
119
120
121
122
123
124
125
126
127
128
 
# File 'lib/adsl/verification/formula_generators.rb', line 116

def binary_op(op, klass, params)
  raise "`#{op}' takes two parameters or none at all" unless params.empty? or params.length == 2
  in_formula_builder do |fb|
    if params.empty?
      fb.adsl_stack << op
    else
      params.each do |param|
        raise "Invalid formula `#{param}' in `#{op}' parameter list" unless param.respond_to? :adsl_ast
      end
      fb.adsl_stack << klass.new(:subformula1 => params.first.adsl_ast, :subformula2 => params.last.adsl_ast)
    end
  end
end

#binary_op_with_any_number_of_params(op, klass, params) ⇒ Object 



103
104
105
106
107
108
109
110
111
112
113
114
 
# File 'lib/adsl/verification/formula_generators.rb', line 103

def binary_op_with_any_number_of_params(op, klass, params)
  in_formula_builder do |fb|
    if params.empty?
      fb.adsl_stack << op
    else
      params.each do |param|
        raise "Invalid formula `#{param}' in `#{op}' parameter list" unless param.respond_to? :adsl_ast
      end
      fb.adsl_stack << klass.new(:subformulae => params.map(&:adsl_ast))
    end
  end
end

#equiv(*params) ⇒ Object 



138
139
140
 
# File 'lib/adsl/verification/formula_generators.rb', line 138

def equiv(*params)
  binary_op_with_any_number_of_params :equiv, ASTEquiv, params
end

#exists(arg_types = {}, &block) ⇒ Object 



69
70
71
 
# File 'lib/adsl/verification/formula_generators.rb', line 69

def exists(arg_types = {}, &block)
  handle_quantifier :exists, ASTExists, arg_types, block
end

#false ⇒ Object 



90
91
92
93
94
 
# File 'lib/adsl/verification/formula_generators.rb', line 90

def false
  in_formula_builder do |fb|
    fb.adsl_stack << false.adsl_ast
  end
end

#forall(arg_types = {}, &block) ⇒ Object 



65
66
67
 
# File 'lib/adsl/verification/formula_generators.rb', line 65

def forall(arg_types = {}, &block)
  handle_quantifier :forall, ASTForAll, arg_types, block
end

#handle_quantifier(quantifier, adsl_ast_node_klass, arg_types, block) ⇒ Object 



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
 
# File 'lib/adsl/verification/formula_generators.rb', line 27

def handle_quantifier(quantifier, adsl_ast_node_klass, arg_types, block)
  raise "A block needs to be passed to quantifiers" if block.nil?
  raise "At least some variables need to be given to the block" if block.parameters.empty?
  in_formula_builder do |fb|
    
    param_types = {}
    block.parameters.each do |param|
      classname = infer_classname_from_varname param[1]
      klass = Object.lookup_const classname
      param_types[param[1].to_sym] = klass
    end
    arg_types.each do |explicit_name, explicit_type|
      classname = classname_for_classname explicit_type
      klass = Object.lookup_const classname
      raise "Unknown class #{explicit_type} for parameter #{explicit_name}" if klass.nil?
      param_types[explicit_name.to_sym] = klass
    end

    param_types.each do |name, klass|
      raise "Unknown klass for variable `#{name}' in #{quantifier} quantifier" if klass.nil?
      raise "Class #{klass.name} is not instrumented" unless klass.respond_to? :adsl_ast
    end

    vars_and_objsets = block.parameters.map{ |param|
      [
        t(param[1].to_s),
        param_types[param[1].to_sym].all.adsl_ast
      ]
    }
    subformula = block.(*block.parameters.map do |param|
      param_types[param[1].to_sym].new :adsl_ast => ASTVariable.new(:var_name => t(param[1]))
    end)
    subformula = true if subformula.nil?
    raise "Invalid formula returned by block in `#{quantifier}'" unless subformula.respond_to? :adsl_ast 
    fb.adsl_stack << adsl_ast_node_klass.new(:vars => vars_and_objsets, :subformula => subformula.adsl_ast)
  end
end

#implies(*params) ⇒ Object 



142
143
144
 
# File 'lib/adsl/verification/formula_generators.rb', line 142

def implies(*params)
  binary_op :implies, ASTImplies, params
end

#in_formula_builder {|formula_builder| ... } ⇒ Object

Yields:

  • (formula_builder) 


15
16
17
18
19
20
21
22
23
24
25
 
# File 'lib/adsl/verification/formula_generators.rb', line 15

def in_formula_builder
  formula_builder = nil
  if self.is_a? ::ADSL::Verification::FormulaBuilder
    formula_builder = self
  else
    formula_builder = ::ADSL::Verification::FormulaBuilder.new
    formula_builder.adsl_stack << self.adsl_ast if self.respond_to? :adsl_ast
  end
  yield formula_builder
  formula_builder
end

#not(param = nil) ⇒ Object Also known as: neg 



73
74
75
76
77
78
79
80
81
 
# File 'lib/adsl/verification/formula_generators.rb', line 73

def not(param = nil)
  in_formula_builder do |fb|
    if param.nil?
      fb.adsl_stack << :not
    else
      fb.adsl_stack << ASTNot.new(:subformula => param.adsl_ast)
    end
  end
end

#or(*params) ⇒ Object 



134
135
136
 
# File 'lib/adsl/verification/formula_generators.rb', line 134

def or(*params)
  binary_op_with_any_number_of_params :or, ASTOr, params
end

#true ⇒ Object 



84
85
86
87
88
 
# File 'lib/adsl/verification/formula_generators.rb', line 84

def true
  in_formula_builder do |fb|
    fb.adsl_stack << true.adsl_ast
  end
end