Index of /~leavens/JML/TeachingMaterial/CAV2007Tutorial/examples

      Name                    Last modified       Size  Description


[DIR] Parent Directory        16-Oct-2007 10:39      -  
[   ] Actor.java              01-Jul-2007 20:54     1k  
[   ] ActorUnderspecified...> 03-Jul-2007 11:59     1k  
[   ] Aging.java              28-Jun-2007 18:08     1k  
[   ] Alias.java              01-Jul-2007 05:01     1k  
[   ] Animal.java             29-Jun-2007 00:58     1k  
[   ] ArrayOps.java           26-Jun-2007 22:43     1k  
[   ] Bag.java                26-Jun-2007 00:31     1k  
[   ] BagOfInt.java           27-Jun-2007 02:26     1k  
[   ] BagOfInt.jml            16-Oct-2007 10:32     1k  
[   ] BagOfInt.jml-refined    05-Jul-2007 11:54     1k  
[   ] BagOfIntMain.java       27-Jun-2007 02:03     1k  
[TXT] BagOfInt_JML_TestDat..> 27-Jun-2007 02:15    11k  
[   ] BoundedStack.java       29-Jun-2007 19:06     1k  
[   ] Counter.java            27-Jun-2007 08:27     1k  
[   ] Counter2.java           27-Jun-2007 20:10     1k  
[   ] DeathException.java     28-Jun-2007 09:20     1k  
[   ] Doctor.java             01-Jul-2007 10:08     1k  
[   ] Ex.java                 30-Jun-2007 14:41     1k  
[   ] Factor.java             01-Jul-2007 10:11     1k  
[   ] FemalePatient.java      11-Aug-2006 12:41     1k  
[   ] Females.java            29-Jun-2007 00:38     1k  
[   ] Gendered.java           29-Jun-2007 19:06     1k  
[   ] GenderedEqualsBad.java  03-Jul-2007 12:00     1k  
[   ] GenderedEqualsGood.java 03-Jul-2007 12:00     1k  
[   ] GreekNoun.java          01-Jul-2007 15:27     1k  
[   ] Hailstone.java          28-Jun-2007 09:20     1k  
[   ] Hailstone2.java         29-Jun-2007 07:39     1k  
[   ] HeadTest.java           01-Jul-2007 10:09     1k  
[   ] Makefile                05-Jul-2007 09:24     2k  
[   ] ModularityDemo.java     30-Jun-2007 12:51     1k  
[   ] Nurse.java              01-Jul-2007 10:08     1k  
[   ] Patient.java            03-Jul-2007 12:16     1k  
[   ] Person.java             11-Aug-2006 01:31     1k  
[   ] Person.refines-jml      03-Jul-2007 12:00     1k  
[   ] PrimeException.java     01-Jul-2007 10:06     1k  
[   ] ScreenPoint.java        30-Jun-2007 14:13     1k  
[   ] ScreenPoint2.java       27-Jun-2007 22:28     1k  
[   ] SortedInts.java         29-Jun-2007 19:06     1k  
[   ] SortedInts2.java        29-Jun-2007 19:06     1k  
[   ] SortedInts3.java        29-Jun-2007 19:06     1k  
[   ] Staff.java              01-Jul-2007 10:09     1k  
[   ] sourceme.sh             27-Jun-2007 01:58     1k  

Some of these examples are from the paper:

   Gary T. Leavens, JML's Rich, Inherited Specifications for
   Behavioral Subtypes.  In Zhiming Liu and He Jifeng (eds), Formal
   Methods and Software Engineering: 8th International Conference on
   Formal Engineering Methods (ICFEM), Macao, China, pages 2-34.
   Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag,
   2006.  The original publication is available at springerlink.com or
   directly from http://dx.doi.org/10.1007/11901433_2.

Those examples are copyright (c) Springer-Verlag, 2006.