Class: ADSL::Extract::Rails::InvariantExtractor

Inherits:
Object
  • Object
show all
Includes:
Verification, Verification::FormulaGenerators, Verification::InstrumentationFilterGenerators
Defined in:
lib/adsl/extract/rails/invariant_extractor.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from Verification::InstrumentationFilterGenerators

#blacklist, #instrumentation_filters

Methods included from Verification::FormulaGenerators

#[], #and, #binary_op, #binary_op_with_any_number_of_params, #equiv, #exists, #false, #forall, #handle_quantifier, #implies, #in_formula_builder, #not, #or, #true

Methods included from Verification::Utils

#classname_for_classname, #infer_classname_from_varname, #t

Constructor Details

#initialize(ar_class_names) ⇒ InvariantExtractor

Returns a new instance of InvariantExtractor.



17
18
19
20
21
22
 
# File 'lib/adsl/extract/rails/invariant_extractor.rb', line 17

def initialize(ar_class_names)
  @ar_class_names = ar_class_names
  @invariants = []
  @builder = nil
  @stack_level = 0
end

Instance Attribute Details

#invariants ⇒ Object (readonly)

Returns the value of attribute invariants.



15
16
17
 
# File 'lib/adsl/extract/rails/invariant_extractor.rb', line 15

def invariants
  @invariants
end

Instance Method Details

#extract(param) ⇒ Object 



35
36
37
38
39
40
41
42
43
44
 
# File 'lib/adsl/extract/rails/invariant_extractor.rb', line 35

def extract(param)
  if param.is_a? Array
    param.each do |path|
      load_in_context path
    end
  else
    ADSL::Extract::Rails::InvariantInstrumenter.new(@ar_class_names).instrument_and_execute_source self, param
  end
  @invariants
end

#invariant(name = nil, builder) ⇒ Object 



24
25
26
 
# File 'lib/adsl/extract/rails/invariant_extractor.rb', line 24

def invariant(name = nil, builder)
  @invariants << Invariant.new(:description => name, :formula => builder.adsl_ast)
end

#load_in_context(path) ⇒ Object 



28
29
30
31
32
33
 
# File 'lib/adsl/extract/rails/invariant_extractor.rb', line 28

def load_in_context(path)
  file = File.open path, 'r'
  ADSL::Extract::Rails::InvariantInstrumenter.new(@ar_class_names).instrument_and_execute_source self, file.read
ensure
  file.close
end