Remove Examples/contract
This set of examples was never tested/documented There is an equivalent testcase in Examples/test-suite/contract.i
This commit is contained in:
parent
e535190c34
commit
bc7a067587
10 changed files with 0 additions and 293 deletions
|
|
@ -1,11 +0,0 @@
|
||||||
#include <stdio.h>
|
|
||||||
|
|
||||||
int Circle (int x, int y, int radius) {
|
|
||||||
/* Draw Circle */
|
|
||||||
printf("Drawing the circle...\n");
|
|
||||||
/* Return -1 to test contract post assertion */
|
|
||||||
if (radius == 2)
|
|
||||||
return -1;
|
|
||||||
else
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
@ -1,19 +0,0 @@
|
||||||
/* File : example.i */
|
|
||||||
|
|
||||||
/* Basic C example for swig contract */
|
|
||||||
/* Tiger, University of Chicago, 2003 */
|
|
||||||
|
|
||||||
%module example
|
|
||||||
|
|
||||||
%contract Circle (int x, int y, int radius) {
|
|
||||||
require:
|
|
||||||
x >= 0;
|
|
||||||
y >= 0;
|
|
||||||
radius > x;
|
|
||||||
ensure:
|
|
||||||
Circle >= 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
%inline %{
|
|
||||||
extern int Circle (int x, int y, int radius);
|
|
||||||
%}
|
|
||||||
|
|
@ -1,17 +0,0 @@
|
||||||
import example
|
|
||||||
# Call the Circle() function correctly
|
|
||||||
|
|
||||||
x = 1;
|
|
||||||
y = 1;
|
|
||||||
r = 3;
|
|
||||||
|
|
||||||
c = example.Circle(x, y, r)
|
|
||||||
|
|
||||||
# test post-assertion
|
|
||||||
x = 1;
|
|
||||||
y = 1;
|
|
||||||
r = 2;
|
|
||||||
|
|
||||||
c = example.Circle(x, y, r)
|
|
||||||
|
|
||||||
print "The return value of Circle(%d, %d, %d) is %d" % (x,y,r,c)
|
|
||||||
|
|
@ -1,20 +0,0 @@
|
||||||
import example
|
|
||||||
|
|
||||||
# Call the Circle() function correctly
|
|
||||||
|
|
||||||
x = 1;
|
|
||||||
y = 1;
|
|
||||||
r = 3;
|
|
||||||
|
|
||||||
c = example.Circle(x, y, r)
|
|
||||||
|
|
||||||
print "The return value of Circle(%d, %d, %d) is %d" % (x,y,r,c)
|
|
||||||
|
|
||||||
# test pre-assertion
|
|
||||||
x = 1;
|
|
||||||
y = -1;
|
|
||||||
r = 3;
|
|
||||||
|
|
||||||
c = example.Circle(x, y, r)
|
|
||||||
|
|
||||||
print "The return value of Circle(%d, %d, %d) is %d" % (x,y,r,c)
|
|
||||||
|
|
@ -1,30 +0,0 @@
|
||||||
#include "example.h"
|
|
||||||
|
|
||||||
#define M_PI 3.14159265358979323846
|
|
||||||
|
|
||||||
/* Move the shape to a new location */
|
|
||||||
void Shape::move(double dx, double dy) {
|
|
||||||
x += dx;
|
|
||||||
y += dy;
|
|
||||||
}
|
|
||||||
|
|
||||||
int Shape::nshapes = 0;
|
|
||||||
|
|
||||||
double Circle::area(void) {
|
|
||||||
/* return -1 is to test post-assertion */
|
|
||||||
if (radius == 1)
|
|
||||||
return -1;
|
|
||||||
return M_PI*radius*radius;
|
|
||||||
}
|
|
||||||
|
|
||||||
double Circle::perimeter(void) {
|
|
||||||
return 2*M_PI*radius;
|
|
||||||
}
|
|
||||||
|
|
||||||
double Square::area(void) {
|
|
||||||
return width*width;
|
|
||||||
}
|
|
||||||
|
|
||||||
double Square::perimeter(void) {
|
|
||||||
return 4*width;
|
|
||||||
}
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
||||||
/* File : example.h */
|
|
||||||
|
|
||||||
class Shape {
|
|
||||||
public:
|
|
||||||
Shape() {
|
|
||||||
nshapes++;
|
|
||||||
}
|
|
||||||
virtual ~Shape() {
|
|
||||||
nshapes--;
|
|
||||||
}
|
|
||||||
double x, y;
|
|
||||||
void move(double dx, double dy);
|
|
||||||
virtual double area(void) = 0;
|
|
||||||
virtual double perimeter(void) = 0;
|
|
||||||
static int nshapes;
|
|
||||||
};
|
|
||||||
|
|
||||||
class Circle : public Shape {
|
|
||||||
private:
|
|
||||||
double radius;
|
|
||||||
public:
|
|
||||||
Circle(double r) : radius(r) { }
|
|
||||||
virtual double area(void);
|
|
||||||
virtual double perimeter(void);
|
|
||||||
};
|
|
||||||
|
|
||||||
class Square : public Shape {
|
|
||||||
private:
|
|
||||||
double width;
|
|
||||||
public:
|
|
||||||
Square(double w) : width(w) { }
|
|
||||||
virtual double area(void);
|
|
||||||
virtual double perimeter(void);
|
|
||||||
};
|
|
||||||
|
|
@ -1,28 +0,0 @@
|
||||||
%module example
|
|
||||||
|
|
||||||
%contract Circle::Circle(double radius) {
|
|
||||||
require:
|
|
||||||
radius > 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
%contract Circle::area(void) {
|
|
||||||
ensure:
|
|
||||||
area > 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
%contract Shape::move(double dx, double dy) {
|
|
||||||
require:
|
|
||||||
dx > 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
/* should be no effect, since there is no move() for class Circle */
|
|
||||||
%contract Circle::move(double dx, double dy) {
|
|
||||||
require:
|
|
||||||
dy > 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
# include must be after contracts
|
|
||||||
%{
|
|
||||||
#include "example.h"
|
|
||||||
%}
|
|
||||||
%include "example.h"
|
|
||||||
|
|
@ -1,33 +0,0 @@
|
||||||
import example
|
|
||||||
|
|
||||||
# Create the Circle object
|
|
||||||
|
|
||||||
r = 2;
|
|
||||||
print " Creating circle (radium: %d) :" % r
|
|
||||||
c = example.Circle(r)
|
|
||||||
|
|
||||||
# Set the location of the object
|
|
||||||
|
|
||||||
c.x = 20
|
|
||||||
c.y = 30
|
|
||||||
print " Here is its current position:"
|
|
||||||
print " Circle = (%f, %f)" % (c.x,c.y)
|
|
||||||
|
|
||||||
# ----- Call some methods -----
|
|
||||||
|
|
||||||
print "\n Here are some properties of the Circle:"
|
|
||||||
print " area = ", c.area()
|
|
||||||
print " perimeter = ", c.perimeter()
|
|
||||||
dx = 1;
|
|
||||||
dy = 1;
|
|
||||||
print " Moving with (%d, %d)..." % (dx, dy)
|
|
||||||
c.move(dx, dy)
|
|
||||||
|
|
||||||
del c
|
|
||||||
|
|
||||||
print "==================================="
|
|
||||||
|
|
||||||
# test construction */
|
|
||||||
r = -1;
|
|
||||||
print " Creating circle (radium: %d) :" % r
|
|
||||||
c = example.Circle(r)
|
|
||||||
|
|
@ -1,44 +0,0 @@
|
||||||
import example
|
|
||||||
|
|
||||||
# Create the Circle object
|
|
||||||
|
|
||||||
r = 2;
|
|
||||||
print " Creating circle (radium: %d) :" % r
|
|
||||||
c = example.Circle(r)
|
|
||||||
|
|
||||||
# Set the location of the object
|
|
||||||
|
|
||||||
c.x = 20
|
|
||||||
c.y = 30
|
|
||||||
print " Here is its current position:"
|
|
||||||
print " Circle = (%f, %f)" % (c.x,c.y)
|
|
||||||
|
|
||||||
# ----- Call some methods -----
|
|
||||||
|
|
||||||
print "\n Here are some properties of the Circle:"
|
|
||||||
print " area = ", c.area()
|
|
||||||
print " perimeter = ", c.perimeter()
|
|
||||||
dx = 1;
|
|
||||||
dy = 1;
|
|
||||||
print " Moving with (%d, %d)..." % (dx, dy)
|
|
||||||
c.move(dx, dy)
|
|
||||||
|
|
||||||
del c
|
|
||||||
|
|
||||||
print "==================================="
|
|
||||||
|
|
||||||
# test area function */
|
|
||||||
r = 1;
|
|
||||||
print " Creating circle (radium: %d) :" % r
|
|
||||||
c = example.Circle(r)
|
|
||||||
# Set the location of the object
|
|
||||||
|
|
||||||
c.x = 20
|
|
||||||
c.y = 30
|
|
||||||
print " Here is its current position:"
|
|
||||||
print " Circle = (%f, %f)" % (c.x,c.y)
|
|
||||||
|
|
||||||
# ----- Call some methods -----
|
|
||||||
|
|
||||||
print "\n Here are some properties of the Circle:"
|
|
||||||
print " area = ", c.area()
|
|
||||||
|
|
@ -1,57 +0,0 @@
|
||||||
import example
|
|
||||||
|
|
||||||
# Create the Circle object
|
|
||||||
|
|
||||||
r = 2;
|
|
||||||
print " Creating circle (radium: %d) :" % r
|
|
||||||
c = example.Circle(r)
|
|
||||||
|
|
||||||
# Set the location of the object
|
|
||||||
|
|
||||||
c.x = 20
|
|
||||||
c.y = 30
|
|
||||||
print " Here is its current position:"
|
|
||||||
print " Circle = (%f, %f)" % (c.x,c.y)
|
|
||||||
|
|
||||||
# ----- Call some methods -----
|
|
||||||
|
|
||||||
print "\n Here are some properties of the Circle:"
|
|
||||||
print " area = ", c.area()
|
|
||||||
print " perimeter = ", c.perimeter()
|
|
||||||
dx = 1;
|
|
||||||
dy = 1;
|
|
||||||
print " Moving with (%d, %d)..." % (dx, dy)
|
|
||||||
c.move(dx, dy)
|
|
||||||
|
|
||||||
del c
|
|
||||||
|
|
||||||
print "==================================="
|
|
||||||
|
|
||||||
# test move function */
|
|
||||||
r = 2;
|
|
||||||
print " Creating circle (radium: %d) :" % r
|
|
||||||
c = example.Circle(r)
|
|
||||||
# Set the location of the object
|
|
||||||
|
|
||||||
c.x = 20
|
|
||||||
c.y = 30
|
|
||||||
print " Here is its current position:"
|
|
||||||
print " Circle = (%f, %f)" % (c.x,c.y)
|
|
||||||
|
|
||||||
# ----- Call some methods -----
|
|
||||||
|
|
||||||
print "\n Here are some properties of the Circle:"
|
|
||||||
print " area = ", c.area()
|
|
||||||
print " perimeter = ", c.perimeter()
|
|
||||||
|
|
||||||
# no error for Circle's pre-assertion
|
|
||||||
dx = 1;
|
|
||||||
dy = -1;
|
|
||||||
print " Moving with (%d, %d)..." % (dx, dy)
|
|
||||||
c.move(dx, dy)
|
|
||||||
|
|
||||||
# error with Shape's pre-assertion
|
|
||||||
dx = -1;
|
|
||||||
dy = 1;
|
|
||||||
print " Moving with (%d, %d)..." % (dx, dy)
|
|
||||||
c.move(dx, dy)
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue