JML

java.security
Class Signature

java.lang.Object
  extended byjava.security.SignatureSpi
      extended byjava.security.Signature

public abstract class Signature
extends SignatureSpi

JML's specification of Signaure.

Author:
Yoonsik Cheon

Class Specifications
initially this.data.isEmpty();
initially java.security.Signature.UNINITIALIZED == 0;
initially java.security.Signature.SIGN == 2;
initially java.security.Signature.VERIFY == 3;
initially this.state == java.security.Signature.UNINITIALIZED;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
 JMLValueSequence data
           
 Key key
           
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
[spec_public] private  String algorithm
           
[spec_public] private  Provider provider
           
[spec_public] protected static int SIGN
           
[spec_public] protected  int state
           
[spec_public] protected static int UNINITIALIZED
           
[spec_public] protected static int VERIFY
           
 
Fields inherited from class java.security.SignatureSpi
appRandom
 
Constructor Summary
protected Signature(non_null String algorithm)
           
 
Model Method Summary
 boolean isPristine()
           
static JMLValueSequence toSeq(byte[] bytes)
           
static JMLValueSequence toSeq(byte[] bytes, int offset, int length)
           
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Object clone()
           
 String getAlgorithm()
           
static Signature getInstance(non_null String algorithm)
           
static Signature getInstance(non_null String algorithm, String provider)
           
static Signature getInstance(String algorithm, non_null Provider provider)
           
 Object getParameter(String param)
          Deprecated. use getParameters()
 AlgorithmParameters getParameters()
           
 Provider getProvider()
           
 void initSign(non_null PrivateKey privateKey)
           
 void initSign(non_null PrivateKey privateKey, non_null SecureRandom random)
           
 void initVerify(non_null Certificate certificate)
           
 void initVerify(non_null PublicKey publicKey)
           
 void setParameter(String param, Object value)
          Deprecated. use setParameter(AlgorithmParameterSpec)
 void setParameter(non_null AlgorithmParameterSpec params)
           
 byte[] sign()
           
 int sign(byte[] outbuf, int offset, int len)
           
 String toString()
           
 void update(byte b)
           
 void update(non_null byte[] data)
           
 void update(non_null byte[] data, int off, int len)
           
 boolean verify(byte[] signature)
           
 boolean verify(byte[] signature, int offset, int length)
           
 
Methods inherited from class java.security.SignatureSpi
engineGetParameter, engineGetParameters, engineInitSign, engineInitSign, engineInitVerify, engineSetParameter, engineSetParameter, engineSign, engineSign, engineUpdate, engineUpdate, engineVerify, engineVerify
 
Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Model Field Detail

data

public JMLValueSequence data
Specifications: non_null

key

public Key key
Field Detail

UNINITIALIZED

protected static final int UNINITIALIZED
Specifications: spec_public

SIGN

protected static final int SIGN
Specifications: spec_public

VERIFY

protected static final int VERIFY
Specifications: spec_public

state

protected int state
Specifications: spec_public

algorithm

private String algorithm
Specifications: spec_public

provider

private Provider provider
Specifications: spec_public
Constructor Detail

Signature

protected Signature(non_null String algorithm)
Specifications:
protected normal_behavior
requires (* algorithm is available *);
assignable this.algorithm;
ensures this.algorithm == algorithm;
ensures_redundantly this.state == java.security.Signature.UNINITIALIZED;
Model Method Detail

toSeq

public static JMLValueSequence toSeq(byte[] bytes)
Specifications: pure
requires bytes != null;

toSeq

public static JMLValueSequence toSeq(byte[] bytes,
                                     int offset,
                                     int length)
Specifications: pure
requires bytes != null&&offset >= 0&&length > 0&&(offset+length) <= bytes.length;

isPristine

public boolean isPristine()
Specifications: pure
Method Detail

getInstance

public static Signature getInstance(non_null String algorithm)
                             throws NoSuchAlgorithmException
Throws:
NoSuchAlgorithmException
Specifications:
public normal_behavior
requires (* algorithm is available *);
assignable \nothing;
ensures \fresh(\result )&&\result .isPristine()&&\result .algorithm == algorithm;
     also
public exceptional_behavior
requires (* algorithm is not available *);
assignable \nothing;
signals (java.security.NoSuchAlgorithmException e) true;

getInstance

public static Signature getInstance(non_null String algorithm,
                                    String provider)
                             throws NoSuchAlgorithmException,
                                    NoSuchProviderException
Throws:
NoSuchAlgorithmException
NoSuchProviderException
Specifications:
public normal_behavior
requires !provider.equals("");
requires (* algorithm is available from provider *);
assignable \nothing;
ensures \fresh(\result )&&\result .isPristine()&&\result .algorithm == algorithm&&\result .provider.getName().equals(provider);
     also
public exceptional_behavior
requires (* provider is not available *);
assignable \nothing;
signals (java.security.NoSuchProviderException e) true;
     also
public exceptional_behavior
requires (* algorithm is not available from provider*);
assignable \nothing;
signals (java.security.NoSuchAlgorithmException e) true;

getInstance

public static Signature getInstance(String algorithm,
                                    non_null Provider provider)
                             throws NoSuchAlgorithmException
Throws:
NoSuchAlgorithmException
Specifications:
public normal_behavior
requires (* algorithm is available from provider *);
assignable \nothing;
ensures \fresh(\result )&&\result .isPristine()&&\result .algorithm == algorithm&&\result .provider == provider;
     also
public exceptional_behavior
requires (* algorithm is not available from provider*);
assignable \nothing;
signals (java.security.NoSuchAlgorithmException e) true;

getProvider

public final Provider getProvider()
Specifications: pure
public normal_behavior
ensures \result == this.provider;

initVerify

public final void initVerify(non_null PublicKey publicKey)
                      throws InvalidKeyException
Throws:
InvalidKeyException
Specifications:
public normal_behavior
requires (* publicKey is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == publicKey&&this.state == java.security.Signature.VERIFY;
     also
public exceptional_behavior
requires (* publicKey is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

initVerify

public final void initVerify(non_null Certificate certificate)
                      throws InvalidKeyException
Throws:
InvalidKeyException
Specifications:
public normal_behavior
requires (* certificate.getPublicKey() is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == certificate.getPublicKey()&&this.state == java.security.Signature.VERIFY;
     also
public exceptional_behavior
requires (* certificate.getPublicKey() is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

initSign

public final void initSign(non_null PrivateKey privateKey)
                    throws InvalidKeyException
Throws:
InvalidKeyException
Specifications:
public normal_behavior
requires (* privateKey is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == privateKey&&this.state == java.security.Signature.SIGN;
     also
public exceptional_behavior
requires (* privateKey is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

initSign

public final void initSign(non_null PrivateKey privateKey,
                           non_null SecureRandom random)
                    throws InvalidKeyException
Throws:
InvalidKeyException
Specifications:
public normal_behavior
requires (* privateKey is valid *);
assignable data, key, state;
ensures this.data.isEmpty()&&this.key == privateKey&&this.state == java.security.Signature.SIGN;
     also
public exceptional_behavior
requires (* privateKey is invalid *);
assignable \nothing;
signals (java.security.InvalidKeyException) true;

sign

public final byte[] sign()
                  throws SignatureException
Throws:
SignatureException
Specifications: non_null
public normal_behavior
requires this.state == java.security.Signature.SIGN;
assignable data;
ensures this.data.isEmpty()&&(* \result is signature of \old(data) *);
     also
public exceptional_behavior
requires this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException) true;

sign

public final int sign(byte[] outbuf,
                      int offset,
                      int len)
               throws SignatureException
Throws:
SignatureException
Specifications:
public normal_behavior
requires this.state == java.security.Signature.SIGN;
assignable data;
ensures this.data.isEmpty()&&(* outbuf[offset..] contains signature of size \result *);
     also
public exceptional_behavior
requires this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException) true;

verify

public final boolean verify(byte[] signature)
                     throws SignatureException
Throws:
SignatureException
Specifications:
public normal_behavior
requires this.state == java.security.Signature.VERIFY&&(* signature improperly encoded *);
assignable data;
ensures this.data.isEmpty()&&\result <==> (* singature is authentic w.r.t. \old(data) *);
     also
public exceptional_behavior
requires this.state != java.security.Signature.VERIFY||(* signature improperly encoded *);
assignable \nothing;
signals (java.security.SignatureException e) true;

verify

public final boolean verify(byte[] signature,
                            int offset,
                            int length)
                     throws SignatureException
Throws:
SignatureException
Specifications:
public normal_behavior
requires offset >= 0&&length > 1&&(offset+length) <= signature.length&&(* signature improperly encoded *);
requires this.state == java.security.Signature.VERIFY;
assignable data;
ensures this.data.isEmpty()&&\result <==> (* singature[offset..offset+length-1] is authentic *);
     also
public exceptional_behavior
requires this.state != java.security.Signature.VERIFY||(* signature improperly encoded *);
assignable \nothing;
signals (java.security.SignatureException e) true;

update

public final void update(byte b)
                  throws SignatureException
Throws:
SignatureException
Specifications:
public normal_behavior
requires this.state == java.security.Signature.VERIFY||this.state == java.security.Signature.SIGN;
assignable data;
ensures this.data.equals(\old(this.data.insertBack(new org.jmlspecs.models.JMLByte(b))));
     also
public exceptional_behavior
requires this.state != java.security.Signature.VERIFY&&this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException e) true;

update

public final void update(non_null byte[] data)
                  throws SignatureException
Throws:
SignatureException
Specifications:
public normal_behavior
requires data.length > 0;
requires this.state == java.security.Signature.VERIFY||this.state == java.security.Signature.SIGN;
assignable this.data;
ensures this.data.equals(\old(this.data.concat(toSeq(data))));
     also
public exceptional_behavior
requires this.state != java.security.Signature.VERIFY&&this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException e) true;

update

public final void update(non_null byte[] data,
                         int off,
                         int len)
                  throws SignatureException
Throws:
SignatureException
Specifications:
public normal_behavior
requires off >= 0&&len > 1&&(off+len) <= data.length;
requires this.state == java.security.Signature.VERIFY||this.state == java.security.Signature.SIGN;
assignable this.data;
ensures this.data.equals(\old(this.data.concat(toSeq(data,off,len))));
     also
public exceptional_behavior
requires this.state != java.security.Signature.VERIFY&&this.state != java.security.Signature.SIGN;
assignable \nothing;
signals (java.security.SignatureException e) true;

getAlgorithm

public final String getAlgorithm()
Specifications: pure
public normal_behavior
ensures \result == this.algorithm;

toString

public String toString()
Overrides:
toString in class Object
Specifications: non_null
Specifications inherited from overridden method in class Object:
       non_null
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
     also
public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
     also
public code model_program { ... }
    implies_that
assignable objectState;
ensures \result != null;

setParameter

public final void setParameter(non_null AlgorithmParameterSpec params)
                        throws InvalidAlgorithmParameterException
Throws:
InvalidAlgorithmParameterException

getParameters

public final AlgorithmParameters getParameters()
Specifications: pure

clone

public Object clone()
             throws CloneNotSupportedException
Overrides:
clone in class SignatureSpi
Throws:
CloneNotSupportedException
Specifications: pure non_null
     also
public normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures (* \result is a clone of this *);
     also
public exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
signals (java.lang.CloneNotSupportedException e) true;
Specifications inherited from overridden method in class Object:
       non_null
protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);
     also
protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));
     also
protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;
     also
protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);

getParameter

public final Object getParameter(String param)
                          throws InvalidParameterException
Deprecated. use getParameters()

Throws:
InvalidParameterException

setParameter

public final void setParameter(String param,
                               Object value)
                        throws InvalidParameterException
Deprecated. use setParameter(AlgorithmParameterSpec)

Throws:
InvalidParameterException

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.