program firstExample {
                    declarations
                    a -> Integer;
                    b -> Integer;
                    c -> Integer;
                    d -> Boolean;
                    pre True; 
                    post ((result != True) && (result != False)); 
                    pre valid_index(e,0)
                    subProgram innerFunction(e -> Array[10]) -> Boolean {
                                                                       declarations
                                                                       f -> Integer;
                                                                       
statements
                                                                       if(e == 0) then  {
                                                                                       f := 0;
                                                                                        }
                                                                                  else  {
                                                                                       f := 1;
                                                                                        }
                                                                       ;
                                                                       return True;
                                                                        };
                    
statements
                    d := innerFunction(a);
                    for(b in 2 to 3) step 1 satisfying (True) {
                                                             write b;
                                                              };
                    for(c in 1 to 10) step 2 satisfying (((c / 4) == 0)) {
                                                                        write c;
                                                                         };
                     }