package testpkg is
    procedure not_guarded(x, y: integer) 
    with pre => x / y > 0;

    procedure guarded_and_then(x, y: integer) 
    with pre => y /= 0 and then x / y > 0;

    procedure guarded_if_then(x, y: integer) 
    with pre => (if y /= 0 then x / y > 0);

    procedure full_guarded(x, y: integer) 
    with pre => (x /= integer'first and y /= -1) and  then x / y > 0 ;

    procedure no_need_for_guarded(x, y: positive) 
    with pre => x / y > 0;
end testpkg;