Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1868] branches/mango/Mango
|
From: <fra...@us...> - 2009-08-30 03:57:22
|
Revision: 1868
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1868&view=rev
Author: frankrimlinger
Date: 2009-08-30 03:57:14 +0000 (Sun, 30 Aug 2009)
Log Message:
-----------
Its always nice when Mango "does something". Here is an example of how errors can be caught. I wrote the following utility to check for the usual array errors:
static public void check(Object array, int index){
if(!array.getClass().getComponentType().isArray()){
throw new IllegalArgumentException();
}
if(index<0 || index>=getLength(array)){
throw new ArrayIndexOutOfBoundsException();
}
}
Here is what mango had to say
Hypothesis: Class-object array is an array
Hypothesis: component class of Class-object array is an array
This is as far as I got, because I just wanted "array" to be an array. Just seeing the same thing written a different way is often enough to break the spell.
Fixed bug where rewriter would fail silently because expected method definition not found in rule base. Now it fails with some noise. This happens for example when an exception is thrown that has not been modelled in the rulebase.
Modelled requisite exception constructors and completed spec for utility method mango.lang.reflect.Mango_Array.check()
Just for the record, including the spec summary here. It is more to read than the original code, true, but the information is organized differently and maybe this is worth something. But even if the final dump of information is worthless, the act of generating it is valuable. So FULL automation is not the goal, the goal is to feed the information at a rate the mind can easily assimilate. (automatic assumptions suppressed, these are too dull to read)
check(Ljava/lang/Object;I)V
cases
Final case. index is less than Array length of array
hypotheses
index is less than Array length of array
index is greater than or equal to 0
Class-object array is an array
array is defined
No return value.
index is greater than or equal to Array length of array
hypotheses
index is greater than or equal to Array length of array
index is greater than or equal to 0
Class-object array is an array
array is defined
Throws: java.lang.ArrayIndexOutOfBoundsException.
Class-object array is not an array
hypotheses
Class-object array is not an array
array is defined
Throws: java.lang.IllegalArgumentException.
index is less than 0
hypotheses
index is less than 0
Class-object array is an array
array is defined
Throws: java.lang.ArrayIndexOutOfBoundsException.
array is undefined
hypotheses
array is undefined
Throws: java.lang.NullPointerException.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/translate/automatic/MethodCallAssumption.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/WorkFlowUtil.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/IllegalStateException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/Mango_Array.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/translate/automatic/MethodCallAssumptionClassObject.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_classObject.java
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ArrayIndexOutOfBoundsException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ArrayIndexOutOfBoundsException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ArrayIndexOutOfBoundsException_MangoFormal/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalArgumentException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalArgumentException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalArgumentException_MangoFormal/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IndexOutOfBoundsException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IndexOutOfBoundsException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IndexOutOfBoundsException_MangoFormal/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/Mango_String/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/Mango_String/formal2nominal(Ljava.lang.String_MangoFormal;)Ljava.lang.String;/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/Mango_String/formal2nominal(Ljava.lang.String_MangoFormal;)Ljava.lang.String;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/Class-object array is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/Final case. index is less than Array length of array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/array is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/index is greater than or equal to Array length of array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/index is less than 0.zip
branches/mango/Mango/mangoUserHome/spec
branches/mango/Mango/mangoUserHome/system/System/java/lang/ArrayIndexOutOfBoundsException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/IllegalArgumentException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/IndexOutOfBoundsException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/RuntimeException_MangoFormal.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
