#267 Add parameter to Unsatisfied Obligation Annotation

open
nobody
None
5
2013-02-05
2012-04-05
Anonymous
No

Using the @CleanupObligation, @CreatesObligation and @DischargesObligation, its currently possible to define create- and discharge pairs for a resource.
I am using these annotations currently for a class which performs two differend kinds of resource allocation:
class MyResourceManager{ //pseudocode
public Object startWork_1(){...}
public Object endWork_1(){...}
public Object startWork_2(){...}
public Object endWork_2(){...}
}

With the current implementation of the Annotation, I can't ensure, that some client code mixes the two kinds of allocation:
client() {
Object o = rm.startWork_1();
try{...}finally{
rm.endWork_2();
}
}

It would be helpful in this case, if the annotations would support some string parameter, which can be used to distinguish between different resources inside the same ResourceManager:

@CleanupObligation
class MyResourceManager{ //pseudocode
@CreatesObligation("case_1") public Object startWork_1(){...}
@DischargesObligation("case_1") public Object endWork_1(){...}
@CreatesObligation("case_2") public Object startWork_2(){...}
@DischargesObligation("case_2") public Object endWork_2(){...}
}

Discussion