@@ -65,7 +65,7 @@ For each write the line with the error, the error and how to fix it
6565
6666Share registration survey
6767
68- - Background data ~~ to 1st survey
68+ - Background data ~~ to 1st survey
6969 - only accept people familiar/very familiar with Java
7070 - Did you contact with LiquidJava before?
7171- Send available date and time for 1h of synchronized study-session, via zoom
@@ -89,44 +89,44 @@ Make a correct and an incorrect use of the annotated code.
8989 int x;
9090 ```
9191
92-
9392
94- - Method annotated - parameters and return. * (Average with parameters dependency)*
93+
94+ - Method annotated - parameters and return. * (Average with parameters dependency)*
9595 Write a correct and an incorrect invocation of function1.
9696
9797 ``` java
9898 @Refinement (" _ >= 0" )
9999 public static double function1(
100- @Refinement (" a >= 0" ) double a,
100+ @Refinement (" a >= 0" ) double a,
101101 @Refinement (" b >= a" ) double b){
102102 return (a + b)/ 2 ;
103103 }
104104 ```
105-
105+
106106- Object State - Vending Machine idea: showing products -> product selected -> pay -> show products
107107Write a correct and incorrect sequence of invocations on the object MyObj
108-
108+
109109 ``` java
110110 @StateSet ({" sX" , " sY" , " sZ" })
111111 public class MyObj {
112-
112+
113113 @StateRefinement (to = " sY(this)" )
114114 public MyObj () {}
115-
115+
116116 @StateRefinement (from = " sY(this)" , to = " sX(this)" )
117117 public void select (int number ) {}
118-
118+
119119 @StateRefinement (from = " sX(this)" , to = " sZ(this)" )
120120 public void pay (int account ) { }
121-
121+
122122 @StateRefinement (from = " sY(this)" , to = " sX(this)" )
123123 @StateRefinement (from = " sZ(this)" , to = " sX(this)" )
124124 public void show () { }
125125 }
126-
126+
127127 ```
128128
129-
129+
130130## PART 2 : Overview
131131
132132Brief introduction to LiquidJava and how to use Refinements in Java.
@@ -143,7 +143,7 @@ Off-video:
143143
144144### 3.1 Plain Java Code
145145
146- Open project without liquid Java.
146+ Open project without liquid Java.
147147
148148Each file contains a bug, try to locate it without running the code.
149149
@@ -155,7 +155,7 @@ For each file answer:
155155
156156### 3.2 Liquid Java Code
157157
158- Open project that contains the liquid-java-api jar and the files already annotated.
158+ Open project that contains the liquid-java-api jar and the files already annotated.
159159
160160Each file contains a bug, try to locate it without running the code.
161161
@@ -194,11 +194,11 @@ This exercises will be grouped in pairs. For each participant, one of the exerci
194194 return n + t1;
195195 }
196196 }
197-
197+
198198 }
199199 ```
200200
201-
201+
202202
203203 * Pair 2 / 2 - * Fibonacci *
204204
@@ -208,7 +208,7 @@ This exercises will be grouped in pairs. For each participant, one of the exerci
208208 /**
209209 * Computes the fibonacci of index n
210210 * @param n The index of the required fibonnaci number
211- * @return The fibonacci nth number. The fibonacci sequence follows the formula Fn = Fn-1 + Fn-2 and has the starting values of F0 = 1 and F1 = 1
211+ * @return The fibonacci nth number. The fibonacci sequence follows the formula Fn = Fn-1 + Fn-2 and has the starting values of F0 = 1 and F1 = 1
212212 */
213213 @Refinement ( " _ >= 1 && GreaterEqualThan(_, n)" )
214214 public static int fibonacci (@Refinement (" Nat(n)" ) int n ){
@@ -220,19 +220,19 @@ This exercises will be grouped in pairs. For each participant, one of the exerci
220220 }
221221 ```
222222
223-
223+
224224
225225* ** 3 ** - State error (using external libs annotated)
226226
227227 * Pair 1 / 2 - Socket , creating object but not connecting/ bind https: // docs.oracle.com/javase/7/docs/api/java/net/Socket.html
228228
229229 ```java
230230 class Test3 {
231-
231+
232232 public void createSocket (InetSocketAddress addr ) throws IOException {
233233 int port = 5000 ;
234- InetAddress inetAddress = InetAddress . getByName(" localhost" );
235-
234+ InetAddress inetAddress = InetAddress . getByName(" localhost" );
235+
236236 Socket socket = new Socket ();
237237 socket. bind(new InetSocketAddress (inetAddress, port));
238238 // missing socket.connect(addr);
@@ -246,30 +246,30 @@ This exercises will be grouped in pairs. For each participant, one of the exerci
246246 @ExternalRefinementsFor (" java.net.Socket" )
247247 @StateSet ({" unconnected" , " binded" , " connected" , " closed" })
248248 public interface SocketRefinements {
249-
249+
250250 @StateRefinement (to = " unconnected(this)" )
251251 public void Socket ();
252-
252+
253253 @StateRefinement (from = " unconnected(this)" ,to = " binded(this)" )
254254 public void bind (SocketAddress add );
255-
255+
256256 @StateRefinement (from = " binded(this)" , to = " connected(this)" )
257257 public void connect (SocketAddress add );
258-
258+
259259 @StateRefinement (from = " connected(this)" )
260260 public void sendUrgentData (int n );
261-
261+
262262 @StateRefinement (to = " closed(this)" )
263263 public void close ();
264-
264+
265265 }
266266 ```
267-
267+
268268 * Pair 2 / 2 - ArrayDeque - To use ghost field size to model the object state (https: // docs.oracle.com/javase/7/docs/api/java/util/ArrayDeque.html)
269269
270270 ```java
271271 class Test3 {
272-
272+
273273 public static void main (String [] args ) throws IOException {
274274 ArrayDeque<Integer > p = new ArrayDeque<> ();
275275 p. add(2 );
@@ -286,42 +286,42 @@ This exercises will be grouped in pairs. For each participant, one of the exerci
286286 ```
287287
288288 ```java
289-
289+
290290 @ExternalRefinementsFor (" java.util.ArrayDeque" )
291291 @Ghost (" int size" )
292292 public interface ArrayDequeRefinements <E> {
293-
293+
294294 public void ArrayDeque ();
295-
295+
296296 @StateRefinement (to = " size(this) == (size(old(this)) + 1)" )
297297 public boolean add (E elem );
298-
298+
299299 @StateRefinement (to = " size(this) == (size(old(this)) + 1)" )
300300 public boolean offerFirst (E elem );
301-
301+
302302 @StateRefinement (from = " size(this) > 0" , to = " size(this) == (size(old(this)))" )
303303 public E getFirst ();
304-
304+
305305 @StateRefinement (from = " size(this) > 0" , to = " size(this) == (size(old(this)))" )
306306 public E getLast ();
307-
307+
308308 @StateRefinement (from = " size(this)> 0" , to = " size(this) == (size(old(this)) - 1)" )
309309 public void remove ();
310-
310+
311311 @StateRefinement (from = " size(this)> 0" , to = " size(this) == (size(old(this)) - 1)" )
312312 public E pop ();
313-
313+
314314 @Refinement (" _ == size(this)" )
315315 public int size ();
316-
316+
317317 @Refinement (" _ == (size(this) <= 0)" )
318318 public boolean isEmpty ();
319-
319+
320320 }
321-
321+
322322 ```
323323
324-
324+
325325
326326
327327
@@ -337,7 +337,7 @@ Each package contains a program to annotate and 2 files with tests (one that sho
337337 ```java
338338 /* A month needs to have a value between 1 and 12*/
339339 int currentMonth;
340-
340+
341341 currentMonth = 13 ;
342342 currentMonth = 5 ;
343343 ```
@@ -355,7 +355,7 @@ Each package contains a program to annotate and 2 files with tests (one that sho
355355 public static int inRange (int a , int b ){
356356 return a + 1 ;
357357 }
358-
358+
359359 public static void main (String [] args ) {
360360 inRange(10 , 11 ); // Correct
361361 inRange(10 , 9 ); // Error
@@ -369,27 +369,27 @@ Each package contains a program to annotate and 2 files with tests (one that sho
369369
370370 ```java
371371 public class TrafficLight {
372-
373- int r;
374- int g;
372+
373+ int r;
374+ int g;
375375 int b;
376-
376+
377377 public TrafficLight () {
378- r = 255 ; g = 0 ; b = 0 ;
378+ r = 255 ; g = 0 ; b = 0 ;
379379 }
380-
380+
381381 public void transitionToAmber () {
382382 r = 255 ; g = 120 ; b = 0 ;
383383 }
384-
384+
385385 public void transitionToGreen () {
386- r = 76 ; g = 187 ; b = 23 ;
386+ r = 76 ; g = 187 ; b = 23 ;
387387 }
388-
388+
389389 public void transitionToRed () {
390- r = 230 ; g = 0 ; b = - 1 ;
390+ r = 230 ; g = 0 ; b = - 1 ;
391391 }
392-
392+
393393 }
394394 ```
395395
@@ -399,9 +399,9 @@ Each package contains a program to annotate and 2 files with tests (one that sho
399399 - [Optional ] What did you dislike the most while using LiquidJava ?
400400 - Would you use LiquidJava in your projects?
401401
402-
403-
404-
402+
403+
404+
405405## EXTRA METHODS - NOT USED
406406
407407* ** 1 ** - Incorrect Invocation Simple Arithmetics
@@ -410,13 +410,13 @@ Each package contains a program to annotate and 2 files with tests (one that sho
410410
411411 ```java
412412 public class Test3 {
413- public static double divide (double numerator ,
413+ public static double divide (double numerator ,
414414 @Refinement (" denominator != 0" )double denominator ){
415415 return numerator/ denominator;
416416 }
417-
417+
418418 public static void main (String [] args ) {
419- double a;
419+ double a;
420420 a = divide(10 , 5 );
421421 a = divide(50 , - 10 + 5 );
422422 a = divide(800 , 2 * 30 - 60 );
@@ -426,29 +426,29 @@ Each package contains a program to annotate and 2 files with tests (one that sho
426426 }
427427 ```
428428
429-
429+
430430
431431 * Part 2 / 2 - * Average Price - only positives*
432432
433433 ```java
434434 public class Test3 {
435435 public static double averagePrice (
436- @Refinement (" price1 >= 0" ) double price1 ,
436+ @Refinement (" price1 >= 0" ) double price1 ,
437437 @Refinement (" price2 >= 0" ) double price2 ){
438438 return (price1 + price2)/ 2 ;
439439 }
440440 public static void main (String [] args ) {
441- double b;
441+ double b;
442442 b = averagePrice(10 , 5 );
443443 b = averagePrice(50 , - 10 + 15 );
444444 b = averagePrice(800 , 2 * 30 - 60 );
445445 b = averagePrice(1952 *- 2 , 20 - 10 );
446- b = averagePrice(5 * 5 * 5 , - 5 *- 1 );
446+ b = averagePrice(5 * 5 * 5 , - 5 *- 1 );
447447 }
448448 }
449449 ```
450-
451-
450+
451+
452452 * Pair 1 / 2 - * Absolute *
453453
454454 ```java
@@ -483,11 +483,7 @@ Each package contains a program to annotate and 2 files with tests (one that sho
483483 if (a > b) // correct: change signal
484484 return b;
485485 else
486- return a;
486+ return a;
487487 }
488488 }
489489 ```
490-
491-
492-
493-
0 commit comments