Some additional examples of ParaSail

Here is a grab-bag of ParaSail examples, with interspersed musings embedded in the comments.  These are acceptable to the ayacc/aflex-based parser posted earlier.

import XXYZ;  // TBD: Does this precede the interface?
              //      Any notion of "use" or "using"
interface Hello_World <Standard_IO<>> is
    procedure Main(IO : ref Standard_IO);
end interface Hello_World;

// TBD: What do enumeration type declarations look like?
//      The first parameter is an id-list type.  The other
//      parameters might be something relating to first/last,
//      'image, etc.

// TBD: What is the comment syntax?  "//" or "--"?  
//      Modula and ML use "(* *)" but ML folks are suggesting
//      the use of "# " as the start of a comment that goes to the EOL.
//      For some reason I find "#" pretty ugly, especially in the
//      middle of a line.
//      C#, C++, and Java all support "//", as well as the
//      partial line '/* ... */'.  That seems error-prone,
//      so sticking with "//" by itself seems simplest.
//      Also "--" means decrement to half the world.

// Syntax:  module::module, type::operation, type::nested_entity,
//          object.component, object.operation [equiv to type::operation(object, ...)]

// TBD: When a non-abstract interface has no module parameters, does that mean
//      the module name can be used directly as a type name?  Or are the "<>"
//      mandatory?  Can we say "interface Univ_Enumeration<> is ..."

// TBD: Should we make aggregates usable when outside the associated class?
//      What about "extension" aggregates?  Operator "aggregate"?

// TBD: Get rid of "subtype" and just use "type Blah is ..." or "type Blah is new ..."
//      "subtype" is a relationship, not a kind of entity.

interface Std <> is

    abstract interface Any<> is
        operator "end" (Obj : ref var Any);
    end interface Any;
    
    abstract interface Assignable<> extends Any is
        operator "copy" Assignable -> Assignable;
    end interface Assignable;

    -- type Univ_Enumeration is ...; // type with all enumerals
    
    type Boolean is Enum <[#false, #true]>; // True or False
    type Ordering is Enum <[#less, #equal, #greater, #unordered]>;

    -- type Univ_Integer is ...; // infinite precision integers with +/- inf
    -- type Univ_Real is ...;    // infinite precision rational numbers 
         // with +/- zero and inf
    -- type Univ_Character is ...;  // ISO 10646, 31-bit character
    -- type Univ_String is ...;  // UTF-32
    
    
end interface Std;

interface Std::Integer<First, Last : Univ_Integer> is
    operator "from_univ"(Univ : Univ_Integer {Univ in First .. Last}) 
      -> Integer;
    operator "to_univ"(Int : Integer) 
      -> Result: Univ_Integer {Result in First .. Last};

    operator "+"(Left, Right : Integer {[[Left]] + [[Right]] in First .. Last}) 
      -> Result : Integer {[[Result]] == [[Left]] + [[Right]]};
end interface Std::Integer;

// [[x]] means "to_univ"(X), as a nod to the double bracket notation used in
// denotational semantics to define the meaning of an expression in a program.


abstract interface Std::Ref<Target_Type is Any<>> 
is
   function Is_Writable(R : Ref) -> Boolean;
   function Exists(R : Ref) -> Boolean;
   function Fetch(R : Ref {Exists(R)}) -> Target_Type;
   procedure Store(R : Ref {Is_Writable(R)}; 
     New_Contents : Target_Type) {Exists(R)};
   procedure Delete(R : Ref {Is_Writable(R)}) {not Exists(R)};
end interface Std::Ref;

class Hello_World <Context<>; Standard_IO<>> is
  exports
    procedure Main(IO : ref Standard_IO) is
       Put_Line(IO.Output, "Hello World");
    end procedure Main;
end class Hello_World;

interface String<Character<>; Index is Integer<>> is
    operator "in"(Lit : Univ_String) -> Boolean;
    operator "from_univ"(Lit : Univ_String {Lit in String}) 
      -> String;
    operator "to_univ"(Str : String) -> Result : Univ_String
      {Result in String};
    operator "~"(Left, Right : String) -> Result : String
      {Length(Result) == Length(Left) + Length(Right)};
end interface String;
      
interface Standard_IO<Context<>; Input_Stream<>; Output_Stream<>> is
    function Output(Context) -> Output_Stream;
    function Input(Context) -> Input_Stream;
end interface Standard_IO;

interface Output_Stream<String<>> is
    procedure Put(Output : ref Output_Stream; Char : String::Character);
    procedure Put(Output : ref Output_Stream; Message : String);
    procedure Put_Line(Output : ref Output_Stream; Message : String);
end interface Output_Stream;

interface Input_Stream<String<>> is
    function Get(Input : ref Input_Stream) -> String::Character;
    function Get_Line(Output : ref Input_Stream) -> String;
end interface Input_Stream;

interface Integer<First, Last : Univ_Integer> is
    operator "in"(Lit : Univ_Integer) -> Result : Boolean 
      {Result == Lit in First .. Last};
    operator "from_univ"(Univ_Integer {Univ_Integer in First .. Last}) 
      -> Integer;
    operator "to_univ"(Integer) -> Result : Univ_Integer 
      {Result in First .. Last};
    operator "+"(Left, Right : Integer 
      {[[Left]] + [[Right]] in First .. Last}) 
      -> Result : Integer
        {[[Result]] == [[Left]] + [[Right]]};
    operator "-"(Left, Right : Integer
      {[[Left]] - [[Right]] in First .. Last}) 
        -> Integer;
    operator "*"(Left, Right : Integer
      {[[Left]] * [[Right]] in First .. Last}) 
        -> Integer;
    operator "/"(Left, Right : Integer
      {[[Left]] / [[Right]] in First .. Last}) 
        -> Integer;
    operator "=?"(Left, Right : Integer) -> Ordering;
end interface Integer;

interface Character<> is
    operator "in"(Lit : Univ_Character) -> Boolean;
    operator "from_univ"(Lit : Univ_Character {Lit in Character}) 
      -> Character;
    operator "to_univ"(Char : Character) 
      -> Result : Univ_Character 
      {Result in Character};
end interface Character;

interface Vector<Component is Assignable<>; 
   First : Univ_Integer := 1;
   Max_Length : Univ_Integer := +inf> is
    function Length(Vec : ref const Vector) -> Univ_Integer 
      {Length in 0..Max_Length};
    function Last(Vec : ref const Vector) -> Univ_Integer 
      {Last == Length(Vec) + First - 1};
    operator "[]"(Vec : ref Vector; Index : Univ_Integer 
      {Index in First..Last(Vec)}) 
      -> ref Component_Type;
    operator "~"(Left, Right : Vector) -> Result : Vector 
      {Length(Left) + Length(Right) == Length(Result)}; 
        // "~" is pronounced "concatenate"
        // or "connect" or "tied to"
        // or "chained to" or "linked to" or ...?
    operator "~"(Left : Vector; Right : Component) -> Result : Vector
      {Length(Left) + 1 == Length(Result)};
    operator "~"(Left : Component; Right : Vector) -> Result : Vector
      {Length(Right) + 1 == Length(Result)};
    operator "~"(Left, Right : Component) -> Result : Vector
      {Length(Result) == 2}; // Do we really need this one?  
                             // Is equivalent to "[Left, Right]"
    operator "null"() -> Result : Vector {Length(Result) == 0};
    procedure Append(Vec : ref mutable Vector; Value : Component)
      {Length(Vec') == Length(Vec) + 1};
    procedure Append(Vec : ref mutable Vector; Other_Vec : Vector)
      {Length(Vec') == Length(Vec) + Length(Other_Vec)}; 
                                        // Vec' means new value
                                        // do we prefer "old(...)"?
                                        // How about post(...) and pre(...)?
                                        // or "new(...)" and "old(...)"?
                                        // Since these are appearing in
                                        // a postcondition, it seems
                                        // redundant to say "post" or "new".
                                        // In any case "new" reads better than post.

    operator ":="(Left : ref var Vector; Right : Vector)
      {Length(Left) == Length(Right)};
      
    operator ":=:"(Left, Right : ref var Vector)
      {Length(Left') == Length(Right) and 
       Length(Right') == Length(Left)};
    operator "+"(Left, Right : Vector {Length(Left) == Length(Right)}) 
      -> Result : Vector
      {Length(Result) == Length(Left)};  // component-wise addition
    
end interface Vector;

interface Stack<Component is Assignable<>; 
  Size_Type is Integer<>> is
    
    function Max_Stack_Size(S : Stack) -> Size_Type 
      {Max_Stack_Size > 0};
    
    function Count(S : Stack) -> Size_Type 
      {Count <= Max_Stack_Size(S)};
    
    function Init(Max : Size_Type {Max > 0}) -> Stack 
      {Max_Stack_Size(Init) == Max and Count(Init) == 0};
    
    function Is_Empty(S : Stack) -> Boolean
      {Is_Empty == (Count(S) == 0)};
    
    function Is_Full(S : Stack) -> Boolean
      {Is_Full == (Count(S) == Mas_Stack_Size(S))};
      
    function Top(S : Stack {not Is_Empty(S)}) -> Component;
    
    procedure Pop(S : ref var Stack {not Is_Empty(S)}) 
      {Count(S') == Count(S) - 1};
      
    procedure Push(S : ref var Stack {not Is_Full(S)}; 
      X : Component) {Count(S') == Count(S) + 1};
      
end interface Stack;