00001 00005 package edu.mit.csail.sdg.squander.regressions; 00006 00007 import junit.framework.Assert; 00008 00009 import org.junit.Test; 00010 00011 import edu.mit.csail.sdg.annotations.Ensures; 00012 import edu.mit.csail.sdg.annotations.Modifies; 00013 import edu.mit.csail.sdg.squander.Squander; 00014 import edu.mit.csail.sdg.squander.annotations.Fresh; 00015 import edu.mit.csail.sdg.squander.annotations.FreshObjects; 00016 00017 public class Tests { 00018 00019 @Ensures("return.length = 2 && null !in return[0] + return[1]") 00020 @Modifies({"return.elems", "return.length"}) 00021 @Fresh({@FreshObjects(cls = Tests[].class, num = 1), @FreshObjects(cls = Tests.class, num = 2)}) 00022 Tests[] make() { 00023 return Squander.exe(this); 00024 } 00025 00026 @Test 00027 public void testMake() { 00028 Object[] m = make(); 00029 Assert.assertNotNull(m); 00030 Assert.assertEquals(2, m.length); 00031 Assert.assertNotNull(m[0]); 00032 Assert.assertNotNull(m[1]); 00033 } 00034 00035 }