Skip to content

Commit

Permalink
Edited contract structure
Browse files Browse the repository at this point in the history
  • Loading branch information
Alex authored and Alex committed Jul 27, 2014
1 parent a66cfba commit 7546a90
Show file tree
Hide file tree
Showing 5 changed files with 166 additions and 38 deletions.
45 changes: 44 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1 +1,44 @@
rdl-0.0.0.gem
{\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210
{\fonttbl\f0\fnil\fcharset0 Consolas;}
{\colortbl;\red255\green255\blue255;\red38\green38\blue38;}
\margl1440\margr1440\vieww10800\viewh8400\viewkind0
\deftab720
\pard\pardeftab720

\f0\fs24 \cf2 # Compiled source #\
###################\
*.com\
*.class\
*.dll\
*.exe\
*.o\
*.so\
\'a0\
# Packages #\
############\
# it's better to unpack these files and commit the raw source\
# git has its own built in compression methods\
*.7z\
*.dmg\
*.gz\
*.iso\
*.jar\
*.rar\
*.tar\
*.zip\
\'a0\
# Logs and databases #\
######################\
*.log\
*.sql\
*.sqlite\
\'a0\
# OS generated files #\
######################\
.DS_Store\
.DS_Store?\
._*\
.Spotlight-V100\
.Trashes\
ehthumbs.db\
Thumbs.db}
4 changes: 2 additions & 2 deletions lib/rdl.rb
Original file line number Diff line number Diff line change
Expand Up @@ -79,12 +79,12 @@ def typesig(mname, sig, meta={})

# Pre condition generator for use in :typesig annotations
def pre(desc=nil,&blk)
PreCtc.new(desc,&blk)
PreCtc.new(RootCtc.new(desc,&blk))
end

# Post condition generator for use in :typesig annotations
def post(desc=nil,&blk)
PostCtc.new(desc,&blk)
PostCtc.new(RootCtc.new(desc,&blk))
end

#
Expand Down
114 changes: 95 additions & 19 deletions lib/rdl_ctc.rb
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@

module RDL

# Interface for Contract Objects
##########################
### Contract Structure ###

class Contract
def apply(*v)
(check *v) ? v : false #(raise "Value(s) #{v.inspect} does not match contract(s) #{self}")
Expand All @@ -19,65 +21,139 @@ def to_proc
def implies(&ctc)
#TODO
end
def getCtcInfo
#TODO Returns inner data for rdoc use; in format where code can recognize contract logic
end
end

# First Order Contract
##########################
### Contract Labelling ###

# Wrapper for Contracts
class CtcLabel < Contract
@ctc = nil
def initialize(wctc)
@ctc = wctc
end
def apply(*v)
@ctc.apply(*v)
end
def check(*v)
@ctc.check(*v)
end
def to_proc
@ctc.to_proc
end
def implies(&ctc)
@ctc.implies(&ctc)
end
end

class PreCtc < CtcLabel
def to_s
"#Pre-Condition : {@ctc.to_s}"
end
end

class PostCtc < CtcLabel
def to_s
"#Post-Condition : #{@ctc.to_s}"
end
end

######################
### Flat Contracts ###

# Contract using user-defined block
class RootCtc < Contract
def initialize(desc="No Description", &ctc)
@pred = ctc
@str = desc
@bindings = [] # TODO: Add node bindings for CbD-CSP
end
def check(*v)
@pred.call unless ((@pred.arity < 0) ? @pred.arity.abs <= v.size : @pred.arity == v.size)
@pred.call(*v) unless ((@pred.arity < 0) ? @pred.arity.abs <= v.size : @pred.arity == v.size)
end
def to_s
"#<RootCtc:#{@str}>"
end
end

# Higher Order Contract Interface
# Shortcut for creating contracts from typesigs
class TypeCtc < RootCtc
def initialize(desc="No Description", typ)
@str = desc
@typeannot = typ
# TODO: Convert TypeAnnot typ into block and assign to @pred
end
end

##############################
### Higher Order Contracts ###

# Inner-node structure for contracts capable of holding multiple child contracts
class OrdNCtc < Contract
@cond = Proc.new{}
def initialize(desc="Blank Contract Bundle: No Description", lctc, rctc)
init()
def initialize(desc="Blank Contract Bundle: No Description", *ctcs)
@str = desc
@lctc = lctc
@rctc = rctc
@ctcls = ctcs
@emp = false
init()
end
def init; end
def check(*v)
@cond.call(lctc.check(*v), rctc, v)
check_aux(v,0)
end
def check_aux(v, nt)
tmp = (nt>=@ctcls.length ? @emp : check(*v,nt+1))
@cond.call(tmp,@ctcls[nt],v)
end
end

# Contract where both child contracts are checked
# Contract where all child contracts must be held
# TODO: Rename AndCtc once deprecated moved
class AandCtc < OrdNCtc
def init
@emp=true
@cond = Proc.new{|l,r,v| l && r.check(*v)}
end
def to_s
"#<ANDCtc:#{@str}>"
end
end

# Contract where one or both child contracts are checked
# Contract where any one child contract must be held
class OrCtc < OrdNCtc
def init
@cond = Proc.new{|l,r,v| }
@cond = Proc.new{|l,r,v| l || r.check(*v)}
end
def to_s
"#<ORCtc:#{@str}>"
end
end

class PreCtc < RootCtc; end

class PostCtc < RootCtc; end


############ TODO: self.convert

# Contract that applies pre(left) and post(right) condition
class MethodCtc < OrdNCtc
def initialize(mname,env,lctc,rctc)
@mname = mname
@env = env.clone
@lctc = lctc
@rctc = rctc
end
def check(*v)
false unless @lctc.check(*v) && @rctc.check(*v,@env.send(@mname.to_sym,*v))
end
def to_s
"#<TypesigMethodCtc:#{@str}>"
end
def rdoc_gen
pg = RDoc::AnyMethod.new("",@mname)
ctx = RDoc::Context.new
# TODO: Implementation
ctx.add_method(pg)

end #TODO: RI support
end

#################################### V DEPRECATED V #######################################

Expand Down
41 changes: 25 additions & 16 deletions lib/rdl_sig.rb
Original file line number Diff line number Diff line change
Expand Up @@ -163,10 +163,6 @@ def typesig(sig, meta={})
RDL::MethodWrapper.wrap_method(@class, mname, old_mname, cls_param_symbols, t)
end

def typeToCtc
#TODO: Implement this
end

# Proposed changes to typesig
def typesig_neo(sig, *ctcmeta)
meta = ((ctcmeta[0].is_a? Hash) ? ctcmeta[0]:{})
Expand Down Expand Up @@ -199,25 +195,24 @@ def typesig_neo(sig, *ctcmeta)
# Handling pre conditions and input types
ctcmeta.each{|typ|
if typ.is_a? Contract
prmctc = ((prmctc && typ.is_a? PreCtc) ? AandCtc.new("User Precondition",typ, prmctc):typ)
retctc = ((retctc && typ.is_a? PostCtc) ? AandCtc.new("User Postcondition",typ, prmctc):typ)
prmctc = ((prmctc && (typ.is_a? PreCtc)) ? AandCtc.new("User Precondition",typ, prmctc):typ)
retctc = ((retctc && (typ.is_a? PostCtc)) ? AandCtc.new("User Postcondition",typ, prmctc):typ)
else
unless typ.is_a? Hash raise RDL::InvalidParameterException, "Invalid input to typesig. Expecting Contract received #{typ.class}!" end
unless (typ.is_a? Hash)
raise RDL::InvalidParameterException, "Invalid input to typesig. Expecting Contract received #{typ.class}!"
end
end
}
t.method_types.each{|typ|
if prmctc
prmctc = AandCtc.new("Input Parameters",typeToCtc(typ), prmctc)
else
prmctc = typeToCtc(typ)
prmctc = TypeCtc.new("Type",typ)
end
}

#TODO: Return Type

pre(prmctc) if prmctc
post(retctc) if retctc

#TODO: Store method

#TODO: Store original value, instance eval or read labelled types
Expand All @@ -226,16 +221,30 @@ def typesig_neo(sig, *ctcmeta)
mname = @mname
old_mname = "__dsl_old_#{mname}"
ti = @class.instance_variable_get(:@typesig_info)
ti[mname] = [@class, mname, old_mname, cls_param_symbols, t]
if t_old
@class.class_eval do
alias_method mname, old_mname
end
ti[mname] = [@class, mname, old_mname, cls_param_symbols, t] #TODO: Put MethodCtc Here

unless @class.instance_methods(false).include?(mname)
#TODO: Alias method_added to call gen_method_wrap
else
gen_method_wrap
end

ensure
@@master_switch = true if status

end
end

def gen_method_wrap(mname)
tempstr = "
def #{mname.to_s} (*args)
return @class.instance_variable_get(:@typesig_info)[-1].check(*v)
end
"
@class.class_eval do
alias_method mname, old_mname
end
@class.class_eval(tempstr)
end


Expand Down
Binary file added rdl-0.0.0.gem
Binary file not shown.

0 comments on commit 7546a90

Please sign in to comment.