101companies

Headline

This Contribution is focussing on exception handling and behavior in Lanugage:JML

Behavior

JML is supporting two types of behavior normal behavior and exceptional behavior, every behavior describes a other "possible" state in the code and has different expectations in the pre/postconditions. Those different cases get connected by the also combinator. So, if one behavior fails in its pre or postcondition,then (when there is one) the next behavior will be tried. In the following example, we use the Feature:Cut and check the two different possibilites, which could occur:

  1. First, the total salarie (using the Feature:Total) is greater than zero, so that the new cutted salarie is also greater than zero.
  2. Second, the total salarie is equal to zero, so that the salarie after the cut is still equal to zero.
/*@ private normal behavior
  @ requires total() == 0;
  @ ensures total() == 0;
  @ also
  @ private normal behavior
  @ requires total() >= 0;
  @ ensures total() >= 0;
  @*/
public void cut(){
    getManager().cut();
	if(getSubdepts() != null)
		for (Department s : getSubdepts())
			s.cut();
		for (Employee e : getEmployees())
			e.cut();
	}

Exceptional Behavior

But, as said above, Language:JML is also supporting exceptional behavior, which allows us to check if some exceptions got to be thrown. Therefore we do not use the normal postcondition keyword "requires" anymore. By exceptional behavior we use signal and signals only. So, if the precondition is true we can define which exception is allowed to be true or false by the signal keyword, while the signals only keyword checks, that just a allowed exceptions had been thrown. In the following example we added to our previous code a exceptional state, which occurs when the total salary is less than zero. In this case we throw a Runtime Exception, which we await to be true in the signals clause and which is the onliest exception which is allowed to be thrown by our signals only clause. 

/*@ private normal behavior
  @ requires totalNoException() == 0;
  @ ensures totalNoException() == 0;
  @ also
  @ private normal behavior
  @ requires totalNoException() >= 0;
  @ ensures totalNoException() >= 0;
  @ also
  @ private exceptional behavior
  @ requires totalNoException() < 0;
  @ signals (RuntimeException e) true; 
  @ signals only RuntimeException;
  @*/
public void cut(){
	if(total() < 0)
		throw new RuntimeException();
    //Rest of function ommited here
}
It is also to say, that JML always accepts those Exceptions, which got declared in the throws-clause of every method.

(C) 2012-2024 softlang.org and contributors

There are no revisions for this page.

User contributions

    This user never has never made submissions.

    User edits

    Syntax for editing wiki

    For you are available next options:

    will make text bold.

    will make text italic.

    will make text underlined.

    will make text striked.

    will allow you to paste code headline into the page.

    will allow you to link into the page.

    will allow you to paste code with syntax highlight into the page. You will need to define used programming language.

    will allow you to paste image into the page.

    is list with bullets.

    is list with numbers.

    will allow your to insert slideshare presentation into the page. You need to copy link to presentation and insert it as parameter in this tag.

    will allow your to insert youtube video into the page. You need to copy link to youtube page with video and insert it as parameter in this tag.

    will allow your to insert code snippets from @worker.

    Syntax for editing wiki

    For you are available next options:

    will make text bold.

    will make text italic.

    will make text underlined.

    will make text striked.

    will allow you to paste code headline into the page.

    will allow you to link into the page.

    will allow you to paste code with syntax highlight into the page. You will need to define used programming language.

    will allow you to paste image into the page.

    is list with bullets.

    is list with numbers.

    will allow your to insert slideshare presentation into the page. You need to copy link to presentation and insert it as parameter in this tag.

    will allow your to insert youtube video into the page. You need to copy link to youtube page with video and insert it as parameter in this tag.

    will allow your to insert code snippets from @worker.