whiley_test_file 0.6.2

original.name="Type_Invalid_14"
js.execute.ignore=true
boogie.ignore=true
boogie.timeout=5
======
>>> main.whiley
type nat is (int x) where x >= 0

// =======================================
// Card Definition
// =======================================

// Suites
final int HEARTS = 1
final int CLUBS = 2
final int DIAMONDS = 3
final int SPADES = 4

// Ordinals
final int TWO = 2
final int THREE = 3
final int FOUR = 4
final int FIVE = 5
final int SIX = 6
final int SEVEN = 7
final int EIGHT = 8
final int NINE = 9
final int TEN = 10
final int JACK = 11
final int QUEEN = 12
final int KING = 13
final int ACE = 14

type Card is { int suite, int ordinal }
// Suite between hearts and clubs
where HEARTS <= suite && suite <= SPADES
// Ordinal between 2 and ACE (high)
where 2 <= ordinal && ordinal <= ACE

// =======================================
// Card Constants
// =======================================

final Card TWO_HEARTS = { suite: HEARTS, ordinal: TWO }
final Card THREE_HEARTS = { suite: HEARTS, ordinal: THREE }
final Card FOUR_HEARTS = { suite: HEARTS, ordinal: FOUR }
final Card FIVE_HEARTS = { suite: HEARTS, ordinal: FIVE }
final Card SIX_HEARTS = { suite: HEARTS, ordinal: SIX }
final Card SEVEN_HEARTS = { suite: HEARTS, ordinal: SEVEN }
final Card EIGHT_HEARTS = { suite: HEARTS, ordinal: EIGHT }
final Card NINE_HEARTS = { suite: HEARTS, ordinal: NINE }
final Card TEN_HEARTS = { suite: HEARTS, ordinal: TEN }
final Card JACK_HEARTS = { suite: HEARTS, ordinal: JACK }
final Card QUEEN_HEARTS = { suite: HEARTS, ordinal: QUEEN }
final Card KING_HEARTS = { suite: HEARTS, ordinal: KING }
final Card ACE_HEARTS = { suite: HEARTS, ordinal: ACE }

final Card TWO_CLUBS = { suite: CLUBS, ordinal: TWO }
final Card THREE_CLUBS = { suite: CLUBS, ordinal: THREE }
final Card FOUR_CLUBS = { suite: CLUBS, ordinal: FOUR }
final Card FIVE_CLUBS = { suite: CLUBS, ordinal: FIVE }
final Card SIX_CLUBS = { suite: CLUBS, ordinal: SIX }
final Card SEVEN_CLUBS = { suite: CLUBS, ordinal: SEVEN }
final Card EIGHT_CLUBS = { suite: CLUBS, ordinal: EIGHT }
final Card NINE_CLUBS = { suite: CLUBS, ordinal: NINE }
final Card TEN_CLUBS = { suite: CLUBS, ordinal: TEN }
final Card JACK_CLUBS = { suite: CLUBS, ordinal: JACK }
final Card QUEEN_CLUBS = { suite: CLUBS, ordinal: QUEEN }
final Card KING_CLUBS = { suite: CLUBS, ordinal: KING }
final Card ACE_CLUBS = { suite: CLUBS, ordinal: ACE }

final Card TWO_DIAMONDS = { suite: DIAMONDS, ordinal: TWO }
final Card THREE_DIAMONDS = { suite: DIAMONDS, ordinal: THREE }
final Card FOUR_DIAMONDS = { suite: DIAMONDS, ordinal: FOUR }
final Card FIVE_DIAMONDS = { suite: DIAMONDS, ordinal: FIVE }
final Card SIX_DIAMONDS = { suite: DIAMONDS, ordinal: SIX }
final Card SEVEN_DIAMONDS = { suite: DIAMONDS, ordinal: SEVEN }
final Card EIGHT_DIAMONDS = { suite: DIAMONDS, ordinal: EIGHT }
final Card NINE_DIAMONDS = { suite: DIAMONDS, ordinal: NINE }
final Card TEN_DIAMONDS = { suite: DIAMONDS, ordinal: TEN }
final Card JACK_DIAMONDS = { suite: DIAMONDS, ordinal: JACK }
final Card QUEEN_DIAMONDS = { suite: DIAMONDS, ordinal: QUEEN }
final Card KING_DIAMONDS = { suite: DIAMONDS, ordinal: KING }
final Card ACE_DIAMONDS = { suite: DIAMONDS, ordinal: ACE }

final Card TWO_SPADES = { suite: SPADES, ordinal: TWO }
final Card THREE_SPADES = { suite: SPADES, ordinal: THREE }
final Card FOUR_SPADES = { suite: SPADES, ordinal: FOUR }
final Card FIVE_SPADES = { suite: SPADES, ordinal: FIVE }
final Card SIX_SPADES = { suite: SPADES, ordinal: SIX }
final Card SEVEN_SPADES = { suite: SPADES, ordinal: SEVEN }
final Card EIGHT_SPADES = { suite: SPADES, ordinal: EIGHT }
final Card NINE_SPADES = { suite: SPADES, ordinal: NINE }
final Card TEN_SPADES = { suite: SPADES, ordinal: TEN }
final Card JACK_SPADES = { suite: SPADES, ordinal: JACK }
final Card QUEEN_SPADES = { suite: SPADES, ordinal: QUEEN }
final Card KING_SPADES = { suite: SPADES, ordinal: KING }
final Card ACE_SPADES = { suite: SPADES, ordinal: ACE }

// =======================================
// DECK
// =======================================

type Deck is (Card[] cards)
// Exactly 52 cards in a deck
where |cards| == 52
// No two cards are the same in a deck
where all { i in 0..|cards|, j in 0..|cards| | (i != j) ==> (cards[i] != cards[j]) }

// A real test of verifier performance!!
final Deck DECK = [
        // Hearts
        TWO_HEARTS,
        THREE_HEARTS,
        FOUR_HEARTS,
        FIVE_HEARTS,
        SIX_HEARTS,
        SEVEN_HEARTS,
        EIGHT_HEARTS,
        NINE_HEARTS,
        TEN_HEARTS,
        JACK_HEARTS,
        QUEEN_HEARTS,
        KING_HEARTS,
        ACE_HEARTS,
        // Clubs
        TWO_CLUBS,
        THREE_CLUBS,
        FOUR_CLUBS,
        FIVE_CLUBS,
        SIX_CLUBS,
        SEVEN_CLUBS,
        EIGHT_CLUBS,
        NINE_CLUBS,
        TEN_CLUBS,
        JACK_CLUBS,
        QUEEN_CLUBS,
        KING_CLUBS,
        ACE_CLUBS,
        // Diamonds
        TWO_DIAMONDS,
        THREE_DIAMONDS,
        FOUR_DIAMONDS,
        FIVE_DIAMONDS,
        SIX_DIAMONDS,
        SEVEN_DIAMONDS,
        EIGHT_DIAMONDS,
        NINE_DIAMONDS,
        TEN_DIAMONDS,
        JACK_DIAMONDS,
        QUEEN_DIAMONDS,
        KING_DIAMONDS,
        ACE_DIAMONDS,
        // Spades
        TWO_SPADES,
        THREE_SPADES,
        FOUR_SPADES,
        FIVE_SPADES,
        SIX_SPADES,
        SEVEN_SPADES,
        EIGHT_SPADES,
        NINE_SPADES,
        TEN_SPADES,
        JACK_SPADES,
        QUEEN_SPADES,
        KING_SPADES,
        ACE_SPADES
    ]

function swap(Deck deck, nat from, nat to) -> Deck
requires from < 52 && to < 52:
    // Swap two cards around
    Card tmp = deck[from]
    deck[from] = deck[to]
    deck[to] = tmp
    //
    return deck

public export method test():
     Deck d = swap(DECK,0,1)
---
E702 main.whiley 168,17:24
E718 main.whiley 168,17:24