Class: Bparity::Formal::Result

Inherits:
Object
  • Object
show all
Defined in:
lib/bparity/formal/result.rb

Constant Summary collapse

VERDICTS = 
%i[no_difference_found difference_found inconclusive].freeze

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(level:, verdict:, scope:, assumptions:, out_of_scope:, counterexample: nil, details: {}) ⇒ Result

Returns a new instance of Result.

Raises:



27
28
29
30
31
32
33
34
35
36
37
38
39
 
# File 'lib/bparity/formal/result.rb', line 27

def initialize(level:, verdict:, scope:, assumptions:, out_of_scope:, counterexample: nil, details: {})
  raise ConfigurationError, "A formal result requires a scope." unless scope
  raise ConfigurationError, "A formal result requires verification assumptions." if assumptions.nil?
  raise ConfigurationError, "Invalid formal verdict: #{verdict}." unless VERDICTS.include?(verdict)

  @level = level.to_s.upcase
  @verdict = verdict
  @scope = scope
  @assumptions = assumptions
  @out_of_scope = out_of_scope
  @counterexample = counterexample
  @details = details
end

Instance Attribute Details

#assumptions ⇒ Object (readonly)

Returns the value of attribute assumptions.



25
26
27
 
# File 'lib/bparity/formal/result.rb', line 25

def assumptions
  @assumptions
end

#counterexample ⇒ Object (readonly)

Returns the value of attribute counterexample.



25
26
27
 
# File 'lib/bparity/formal/result.rb', line 25

def counterexample
  @counterexample
end

#details ⇒ Object (readonly)

Returns the value of attribute details.



25
26
27
 
# File 'lib/bparity/formal/result.rb', line 25

def details
  @details
end

#level ⇒ Object (readonly)

Returns the value of attribute level.



25
26
27
 
# File 'lib/bparity/formal/result.rb', line 25

def level
  @level
end

#out_of_scope ⇒ Object (readonly)

Returns the value of attribute out_of_scope.



25
26
27
 
# File 'lib/bparity/formal/result.rb', line 25

def out_of_scope
  @out_of_scope
end

#scope ⇒ Object (readonly)

Returns the value of attribute scope.



25
26
27
 
# File 'lib/bparity/formal/result.rb', line 25

def scope
  @scope
end

#verdict ⇒ Object (readonly)

Returns the value of attribute verdict.



25
26
27
 
# File 'lib/bparity/formal/result.rb', line 25

def verdict
  @verdict
end

Instance Method Details

#success? ⇒ Boolean

Returns:

  • (Boolean) 


47
 
# File 'lib/bparity/formal/result.rb', line 47

def success? = verdict == :no_difference_found

#to_h ⇒ Object 



41
42
43
44
45
 
# File 'lib/bparity/formal/result.rb', line 41

def to_h
  { "level" => level, "verdict" => verdict.to_s, "scope" => scope.to_h,
    "assumptions" => assumptions.map(&:to_s), "out_of_scope" => out_of_scope,
    "counterexample" => counterexample, "details" => details }
end