Type assertions, typeOf

Another interface from the image package of the Go standard library is the Model, to convert between different color models. In this section, we study an implementation of this interface using both type assertions and the typeOf function from Gobra.

// Model can convert any [Color] to one from its own color model. The conversion
// may be lossy.
type Model interface {
	// @ requires c != nil
	// @ ensures res != nil
	Convert(c Color) (res Color)
}

// without specifications for simplicity
type Color interface {
	RGBA() (r, g, b, a uint32)
}

We cannot convert any color as described in the docstring, but any color with c != nil to exclude the case of the nil interface value.

Type assertions

Given an interface value v of underlying type T, we can recover the concrete value i of type T using a type assertion i := v.(T). This operation might cause a run-time panic when the underlying type is not T. In the following example, Gobra reports an error since the underlying type of the variable c is unknown:

// @ requires c != nil
func TypeAssertion(c Color) {
	c1 := c.(Alpha16) // error
	r, g, b, a := c1.RGBA()
	// @ assert r == g
}

ERROR Type assertion might fail. 

Dynamic value might not be a subtype of the target type.

By assigning a second variable i, ok := v.(T), the type assertion no longer panics. If ok is true then i is the underlying value. Otherwise, if ok is false, i is the zero value of type T.

Consider the implementation of the Model interface for the alpha16Model, which converts a color to the Alpha16 color model. By using a type assertion, we can return the argument if it is already an Alpha16 color:

type alpha16Model struct{}

var Alpha16Model alpha16Model

// @ requires c != nil
// @ ensures res != nil
// @ ensures typeOf(res) == type[Alpha16]
func (_ alpha16Model) Convert(c Color) (res Color) {
	if _, ok := c.(Alpha16); ok {
		return c
	}
	_, _, _, a := c.RGBA()
	return Alpha16{uint16(a)}
}

Dynamic types with typeOf

Gobra provides the typeOf function, which takes an argument of an interface value and returns its dynamic type. In the example above, we specified in the Convert implementation of alpha16Model that the return type is Alpha16. Note that to implement the Model interface, the return type must be Color, not Alpha16.

// @ ensures typeOf(res) == type[Alpha16]

To refer to it, we must wrap the type T with type[T]. With this postcondition, the following client code verifies:

func converting() {
	c1 := Constant{}
	c2 := Alpha16Model.Convert(c1)
	c3 := c2.(Alpha16)
	c3.RGBA()
}

Full section example

package main

// without specifications for simplicity
type Color interface {
	RGBA() (r, g, b, a uint32)
}


type Alpha16 struct {
	A uint16
}

type Constant struct{}

// @ ensures r == 0x0 && g == 0xffff && b == 0xffff && a == 0xffff
func (c Constant) RGBA() (r, g, b, a uint32) {
	return 0x0, 0xffff, 0xffff, 0xffff
}

func (c Alpha16) RGBA() (r, g, b, a uint32) {
	a = uint32(c.A)
	return a, a, a, a
}


// Model can convert any [Color] to one from its own color model. The conversion
// may be lossy.
type Model interface {
	// @ requires c != nil
	// @ ensures res != nil
	Convert(c Color) (res Color)
}


func converting() {
	c1 := Constant{}
	c2 := Alpha16Model.Convert(c1)
	c3 := c2.(Alpha16)
	c3.RGBA()
}


type alpha16Model struct{}

var Alpha16Model alpha16Model

// @ requires c != nil
// @ ensures res != nil
// @ ensures typeOf(res) == type[Alpha16]
func (_ alpha16Model) Convert(c Color) (res Color) {
	if _, ok := c.(Alpha16); ok {
		return c
	}
	_, _, _, a := c.RGBA()
	return Alpha16{uint16(a)}
}

// @ alpha16Model implements Model