PK ]eGX9
^ ^ app.ecf
/EIFGENs$/.svn$/CVS$
PK ]eG addition_strategy.eclass
ADDITION_STRATEGY
inherit
OPERATOR_STRATEGY
feature -- Basic operations
execute (a, b: INTEGER)
--
do
last_result := a + b
ensure then
last_result = a + b
end
end
PK ]eG+;o autoproof.pyimport sys
import os, os.path
import shutil
import time
from subprocess import call
# EXAMPLE SPECIFIC
ap_options = [
'-ownership',
'-postpredicate',
'-timeout', '120']
# GENERAL (changes here have to be copied to all other autoproof.py files)
# environment variables
os.environ['ISE_PLATFORM'] = 'win64'
os.environ['ISE_C_COMPILER'] = 'msc'
os.environ['ISE_EIFFEL'] = "C:\\Eiffel\\eve"
os.environ['ISE_LIBRARY'] = os.getenv("ISE_EIFFEL")
os.environ['ISE_PRECOMP'] = os.path.join(os.getenv("ISE_EIFFEL"), 'precomp', 'spec', 'win64')
os.environ['PATH'] = os.path.join(os.getenv("ISE_EIFFEL"), 'studio', 'tools', 'boogie') + os.pathsep + os.path.join(os.getenv("ISE_EIFFEL"), 'studio', 'spec', os.getenv("ISE_PLATFORM"), 'bin') + os.pathsep + os.environ['PATH']
# change to specific directory
path = sys.argv[-1]
dir, fn = os.path.split(os.path.abspath(path))
os.chdir(dir)
# check for default ecf, target and options
if not 'ecf_name' in locals():
for f in os.listdir('.'):
base = os.path.basename(f)
file, ext = os.path.splitext(base)
if ext == '.ecf':
ecf_name = base
target_name = file
# ec options
args = ['-batch',
'-output_file', 'out.txt',
'-project', ecf_name,
'-target', target_name,
'-batch',
'-boogie', '-html'] + ap_options
# call eve
call(["ec.exe"] + args)
PK ]eG client.eclass
CLIENT
feature
test_strategy
-- Demo for strategy classes.
local
s1, s2: OPERATOR_STRATEGY
do
create {ADDITION_STRATEGY} s1
create {SUBTRACTION_STRATEGY} s2
s1.execute (3, 4)
s2.execute (9, 2)
check s1.last_result = s2.last_result end
end
end
PK ]eGV operator_strategy.edeferred class
OPERATOR_STRATEGY
feature -- Access
last_result: INTEGER
-- Result of last execution.
feature -- Basic operations
execute (a, b: INTEGER)
-- Execute operator strategy.
deferred
end
end
PK ]eG$
readme.txtTitle: Strategy
Category: Design Pattern
Source: [FAC'07](http://dl.acm.org/citation.cfm?id=1272668)
Abstract: A program's behaviour is selected at runtime (design pattern).
Description:
The abstract strategy class has an operation that gets refined in different subclasses. The client can write client code operating with the abstract class, while instantiating the entities with specific subclasses. Then the reasoning has to deal with the dynamic representation.
PK ]eGy subtraction_strategy.eclass
SUBTRACTION_STRATEGY
inherit
OPERATOR_STRATEGY
feature -- Basic operations
execute (a, b: INTEGER)
--
do
last_result := a - b
ensure then
last_result = a - b
end
end
PK ]eGX9
^ ^ app.ecfPK ]eG addition_strategy.ePK ]eG+;o autoproof.pyPK ]eG
client.ePK ]eGV operator_strategy.ePK ]eG$
readme.txtPK ]eGy subtraction_strategy.ePK