spec: type assertions and type switches must be valid

The spec didn't preclude invalid type assertions and
type switches, i.e., cases where a concrete type doesn't
implement the interface type in the assertion in the first
place. Both, the gc and gccgo compiler exclude these cases.
This is documenting the status quo.

Also:
- minor clean up of respective examples
- added sentence about default case in select statements

Fixes #4472.

R=rsc, iant, r, ken
CC=golang-dev
https://golang.org/cl/6869050

doc/go_spec.html

@@ -1,6 +1,6 @@
 <!--{
 	"Title": "The Go Programming Language Specification",
-	"Subtitle": "Version of December 4, 2012",
+	"Subtitle": "Version of December 6, 2012",
 	"Path": "/ref/spec"
 }-->
 
@@ -2668,8 +2668,11 @@ The notation <code>x.(T)</code> is called a <i>type assertion</i>.
 More precisely, if <code>T</code> is not an interface type, <code>x.(T)</code> asserts
 that the dynamic type of <code>x</code> is <a href="#Type_identity">identical</a>
 to the type <code>T</code>.
+In this case, <code>T</code> must <a href="#Method_sets">implement</a> the (interface) type of <code>x</code>;
+otherwise the type assertion is invalid since it is not possible for <code>x</code>
+to store a value of type <code>T</code>.
 If <code>T</code> is an interface type, <code>x.(T)</code> asserts that the dynamic type
-of <code>x</code> implements the interface <code>T</code> (§<a href="#Interface_types">Interface types</a>).
+of <code>x</code> implements the interface <code>T</code>.
 </p>
 <p>
 If the type assertion holds, the value of the expression is the value
@@ -2679,8 +2682,19 @@ In other words, even though the dynamic type of <code>x</code>
 is known only at run time, the type of <code>x.(T)</code> is
 known to be <code>T</code> in a correct program.
 </p>
+
+<pre>
+var x interface{} = 7  // x has dynamic type int and value 7
+i := x.(int)           // i has type int and value 7
+
+type I interface { m() }
+var y I
+s := y.(string)        // illegal: string does not implement I (missing method m)
+r := y.(io.Reader)     // r has type io.Reader and y must implement both I and io.Reader
+</pre>
+
 <p>
-If a type assertion is used in an assignment or initialization of the form
+If a type assertion is used in an <a href="#Assignments">assignment</a> or initialization of the form
 </p>
 
 <pre>
@@ -2696,7 +2710,7 @@ otherwise, the expression returns <code>(Z, false)</code> where <code>Z</code>
 is the <a href="#The_zero_value">zero value</a> for type <code>T</code>.
 No run-time panic occurs in this case.
 The type assertion in this construct thus acts like a function call
-returning a value and a boolean indicating success.  (§<a href="#Assignments">Assignments</a>)
+returning a value and a boolean indicating success.
 </p>
 
 
@@ -4159,9 +4173,20 @@ case x == 4: f3()
 A type switch compares types rather than values. It is otherwise similar
 to an expression switch. It is marked by a special switch expression that
 has the form of a <a href="#Type_assertions">type assertion</a>
-using the reserved word <code>type</code> rather than an actual type.
-Cases then match literal types against the dynamic type of the expression
-in the type assertion.
+using the reserved word <code>type</code> rather than an actual type:
+</p>
+
+<pre>
+switch x.(type) {
+// cases
+}
+</pre>
+
+<p>
+Cases then match actual types <code>T</code> against the dynamic type of the
+expression <code>x</code>. As with type assertions, <code>x</code> must be of
+<a href="#Interface_types">interface type</a>, and each non-interface type
+<code>T</code> listed in a case must implement the type of <code>x</code>.
 </p>
 
 <pre class="ebnf">
@@ -4197,17 +4222,17 @@ the following type switch:
 <pre>
 switch i := x.(type) {
 case nil:
-	printString("x is nil")
+	printString("x is nil")                // type of i is type of x (interface{})
 case int:
-	printInt(i)  // i is an int
+	printInt(i)                            // type of i is int
 case float64:
-	printFloat64(i)  // i is a float64
+	printFloat64(i)                        // type of i is float64
 case func(int) float64:
-	printFunction(i)  // i is a function
+	printFunction(i)                       // type of i is func(int) float64
 case bool, string:
-	printString("type is bool or string")  // i is an interface{}
+	printString("type is bool or string")  // type of i is type of x (interface{})
 default:
-	printString("don't know the type")
+	printString("don't know the type")     // type of i is type of x (interface{})
 }
 </pre>
 
@@ -4218,22 +4243,23 @@ could be rewritten:
 <pre>
 v := x  // x is evaluated exactly once
 if v == nil {
+	i := v                                 // type of i is type of x (interface{})
 	printString("x is nil")
 } else if i, isInt := v.(int); isInt {
-	printInt(i)  // i is an int
+	printInt(i)                            // type of i is int
 } else if i, isFloat64 := v.(float64); isFloat64 {
-	printFloat64(i)  // i is a float64
+	printFloat64(i)                        // type of i is float64
 } else if i, isFunc := v.(func(int) float64); isFunc {
-	printFunction(i)  // i is a function
+	printFunction(i)                       // type of i is func(int) float64
 } else {
-	i1, isBool := v.(bool)
-	i2, isString := v.(string)
+	_, isBool := v.(bool)
+	_, isString := v.(string)
 	if isBool || isString {
-		i := v
-		printString("type is bool or string")  // i is an interface{}
+		i := v                         // type of i is type of x (interface{})
+		printString("type is bool or string")
 	} else {
-		i := v
-		printString("don't know the type")  // i is an interface{}
+		i := v                         // type of i is type of x (interface{})
+		printString("don't know the type")
 	}
 }
 </pre>
@@ -4501,7 +4527,8 @@ If any of the resulting operations can proceed, one of those is
 chosen and the corresponding communication and statements are
 evaluated.  Otherwise, if there is a default case, that executes;
 if there is no default case, the statement blocks until one of the communications can
-complete.
+complete. There can be at most one default case and it may appear anywhere in the
+"select" statement.
 If there are no cases with non-<code>nil</code> channels,
 the statement blocks forever.
 Even if the statement blocks,