gistfile1.txt

// simple.k

module SIMPLE-SYNTAX

endmodule

module SIMPLE
  
  imports BOOL
  imports INT

  syntax Bitfield ::= Bitfield Bit
                    | Bit

  syntax Bit ::= "l" | "h"

  syntax Int ::= bToI(Bit) [function]
               | bfToI(Bitfield) [function]

  rule bToI(l:Bit) => 0
  rule bToI(h:Bit) => 1

  rule bfToI(XS:Bitfield X:Bit) => (bfToI(XS) *Int 2) +Int bToI(X)
  rule bfToI(X:Bit) => bToI(X)

endmodule

// simple-spec.k

module SIMPLE-SPEC
    imports SIMPLE
    
    rule <k> bfToI(XS) => 5</k>

endmodule

// kprove simple-spec.k
  #Not ( {
    5
  #Equals
    bfToI ( XS )
  } )
#And
  <k>
    bfToI ( XS )
  </k>