WLS: Adds description of field access.

Also tidies up the issue of indirect invocation.

Author: DavePearce

WhileyLanguageSpecification/examples/ch6/eg_14.whiley

@@ -5,4 +5,4 @@ method length(LinkedList l) -> int:
     if l is null:
         return 0
     else:
-        return 1 + length((*l).next)
+        return 1 + length(l->next)

WhileyLanguageSpecification/examples/ch6/eg_23.whiley

@@ -0,0 +1,4 @@
+type Vec is {int x, int y, int z}
+
+function dotProduct(Vec v1, Vec v2) -> Vec:
+    return (v1.x * v2.x) + (v1.y * v2.y) + (v1.z * v2.z)

WhileyLanguageSpecification/src/WhileyLanguageSpec.pdf

@@ -251,12 +251,13 @@ \section{Equality Expressions}
 
 \section{Invoke Expressions}
 \label{c_expr_invoke}
-An {\em function or method invocation} executes a named function or method declared in a given source file.  An invocation passes arguments of appropriate number and type to the executed function or method.  An invocation may also return one or more values which can be subsequently used.
+An {\em function or method invocation} executes a named function or method declared in a given source file.  An {\em indirection function or method invocation} executes a function determined by a given expression.  An invocation passes arguments of appropriate number and type to the executed function or method.  An invocation may also return one or more values which can be subsequently used.
 
 % Could also discuss function or method lookup; this is really part of typing.
 
 \begin{syntax}
   \verb+InvokeExpr+ & $::=$ & \verb+Name+ \token{(} \verb+ArgsList+ \token{)}\\
+  \verb+IndirectInvokeExpr+ & $::=$ & \verb+UnitExpr+\ \token{(}\ \verb+ArgsList+\ \token{)}\\
 &&\\
 \verb+ArgsList+ & $::=$ & \big[\ \verb+UnitExpr+\ \big(\ \token{,}\ \verb+UnitExpr+\ \big)$^*$\ \big]\\
 \end{syntax}
@@ -490,7 +491,6 @@ \subsection{List Constructors}
 \section{Record Expressions}
 \label{c_expr_record}
 
-
 Record expressions operate on values of record type (e.g. \lstinline|{int x, int y}|, etc).
 
 % =======================================================================
@@ -500,21 +500,17 @@ \section{Record Expressions}
 \subsection{Field Access Expressions}
 \label{c_expr_field_access}
 
+The field access operator accepts a value of record type and returns the value held in a given field.
+
 \begin{syntax}
-  \verb+FieldAccessExpr+ & $::=$ & \verb+UnitExpr+\\
-   &  \big( &\token{.}\ \verb+Ident+\ \big[\ \token{(}\ \verb+ArgsList+\ \token{)}\ \big]\\
-   & $|$ & \token{->}\ \verb+Ident+\ \big[\ \token{(}\ \verb+ArgsList+\ \token{)}\ \big]\\
-   & \big)$^+$&\\
+  \verb+FieldAccessExpr+ & $::=$ & \verb+UnitExpr+\ \token{.}\ \verb+Ident+\\
 \end{syntax}
 
-\paragraph{Description.}
-
-The {\em arrow operator} returns a field of the value referenced by the argument.
+\paragraph{Examples.}  The following example illustrates a field access expression constructor:
 
-\paragraph{Examples.}
-
-\paragraph{Notes.} The arrow operation ``\lstinline{e->f}'' is a short-hand notation for ``\lstinline{(*e).f}'' and can be used when \lstinline{e} has effective record type (\S\ref{c_types_effective_records}).
+\lstinputlisting{../examples/ch6/eg_23.whiley}
 
+The above function computes the so-called {\em dot product} of two vectors.  The field access operator is used to access the three fields of each vector. 
 
 % =======================================================================
 % Record Expression
@@ -563,11 +559,11 @@ \subsection{New Expressions}
 \subsection{Dereference Expressions}
 \label{c_expr_dereference}
 
-A {\em dereference expression} accepts an argument of reference type and returns a value (or element) of the reference's target type.  The {\em dereference operator} returns the value referenced by the argument.  
+A dereference expression accepts an argument of reference type and returns a value (or element) of the reference's target type.  The {\em dereference operator} returns the value referenced by the argument.  The {\em arrow operator} returns a field of the value referenced by the argument.
 
 \begin{syntax}
-  \verb+DereferenceExpr+ & $::=$ & \token{*}\ \verb+TermExpr+\\\
-  & $|$ & \verb+TermExpr+\ \token{->}\ \verb+Identifier+\\
+  \verb+DereferenceExpr+ & $::=$ & \token{*}\ \verb+TermExpr+\\
+  & $|$ & \verb+UnitExpr+\ \token{->}\ \verb+Ident+\ \big[\ \token{(}\ \verb+ArgsList+\ \token{)}\ \big]\\
 \end{syntax}
 
 \paragraph{Example.} The following illustrates the dereference operator:
@@ -576,7 +572,8 @@ \subsection{Dereference Expressions}
 
 This function traverses a linked list counting the number of links it contains.  The arrow operator is used to access the next link in the chain.
 
-\paragraph{Notes.}
+\paragraph{Notes.} The arrow operation ``\lstinline{e->f}'' is a short-hand notation for ``\lstinline{(*e).f}'' and can be used when \lstinline{*e} has effective record type (\S\ref{c_types_effective_records}).
+
 
 % =======================================================================
 % Term Expressions