Pierre Letouzey
email: pierre.letouzey@ens.fr

Laurent Théry
email: laurent.thery@sophia.inria.fr

Formalizing Stålmarck's algorithm in Coq

Keywords: Parameter gen: ∀n: nat, ∀A: Set, ∀f: nat

We present the development of a machine-checked implementation of Stålmarck's algorithm. First, we prove the correctness and the completeness of an abstract representation of the algorithm. Then, we give an effective implementation of the algorithm that we prove correct.

A The predicate for one-step propagation

→ & p-q : ∀p, q, r: rZ . ∀S: State. p ∼ S -q ⇒ S → p:=q & r (q, )+(r , ⊥)+S | → & p-r : ∀p, q, r: rZ .

Introduction

When formalizing an algorithm inside a prover, every single step has to be justified. The result is a presentation of the algorithm where no detail has been omitted. Mechanizing the proofs of correctness and completeness is the main goal of this formalization. Whenever such proofs are intricate and involve a large amount of case exploration, mechanized proofs may be an interesting complement to the ones on paper. Also, there is often a gap between an algorithm and its actual implementation. Bridging this gap formally and getting a reasonably efficient certified implementation is a valuable exercise.

In this paper we explain how this has been done for Stålmarck's algorithm [START_REF] Sheeran | A tutorial on Stålmarck's proof procedure for propositional logic[END_REF] using the Coq prover [START_REF] Huet | The Coq Proof Assistant: A Tutorial: Version 6[END_REF]. This algorithm is a tautology checker. It is patented and has been successfully applied in industry. As it includes a number of heuristics, what we formalize is an abstract version of the algorithm. We prove different properties of the algorithm including correctness and completeness. We also cover two ways of ensuring that the result of an implementation is correct. We define execution traces and prove that these traces can be used to check that a formula is a tautology in a more elementary way. We also derive a certified implementation.

The paper is structured as follows. The algorithm is presented in Section 2. The formalization of the algorithm is described in Section 3. The notion of trace is introduced in Section 4. Finally the implementation is given in Section 5.

The algorithm

Stålmarck's algorithm is a tautology checker. It deals with boolean formulae, i.e. expressions formed with the two constants (true), ⊥ (false), the unary symbol ¬ (negation), the binary symbols & (conjunction), # (disjunction), → (implication), = (equivalence), and a set of variables (v i ) i∈N . For example, the

v 1 v 3 & v2 v4 & ¬ & v 3 v 4 ¬ & ¬ v 1 v 2 ¬ ¬ & v & 5 6 7 ¬ & v v v 8 v 9 v 10 v 11
Fig. 1. Annotated tree-like representation of the formula following formula is a boolean expression containing four variables v 1 , v 2 , v 3 and v 4 :

((v 1 → v 2 ) & (v 3 → v 4 )) → ((v 1 & v 3 ) → (v 2 & v 4 ))
It is also a tautology. This means that the formula is valid (true) for any value of its variables. The first step of the algorithm is to reduce the number of binary symbols using the following equalities:

A # B = ¬(¬A & ¬B) A → B = ¬(A & ¬B) ¬¬A = A
With this transformation, we obtain an equivalent formula containing only conjunctions, equalities and negations. By applying this transformation on our example, we get:

¬((¬(v 1 & ¬v 2 ) & ¬(v 3 & ¬v 4 )) & ((v 1 & v 3 ) & ¬(v 2 & v 4 )))
The algorithm manipulates data structures called triplets. To handle negation, variables are signed: ±v i . A triplet is a group of three signed variables and a connector (either & or =), meaning that the first variable has the value of the result of applying the connector to the other two variables. The two kinds of triplets are written as v i := ±v j & ± v k and v i := ±v j = ±v k . Every reduced boolean expression has a corresponding list of triplets. If we consider the tree representation of the formula and annotate every binary tree with a fresh new variable as in Figure 1, taking every binary node of the annotated tree to form a triplet gives us the list of triplets representing the formula. In our example, we get the following list:

v 5 := v 1 & -v 2 (1) v 6 := v 3 & -v 4 (2) v 7 := -v 5 & -v 6 (3) v 8 := v 1 & v 3 (4) v 9 := v 2 & v 4 (5) v 10 := v 8 & -v 9 (6) v 11 := v 7 & v 10 (7)
The value of the formula is the value of -v 11 . The algorithm works by refutation. It assumes that the formula is false and tries to reach a contradiction by propagation. There is a set of rules for each kind of triplets that defines how to do this propagation. For the triplet v i := v j & v k we have nine rules:

if v i =-v j , propagate v j = and v k = ⊥ & i-j if v i =-v k , propagate v j = ⊥ and v k = & i-k if v j = v k , propagate v i = v k & jk if v j =-v k , propagate v i = ⊥ & j-k if v i = , propagate v j = and v k = & i if v j = , propagate v i = v k & j if v j = ⊥, propagate v i = ⊥ & j⊥ if v k = , propagate v i = v j & k if v k = ⊥, propagate v i = ⊥ & k⊥
For the triplet v i := v j = v k we have twelve rules:

if v i = v j , propagate v k = = ij if v i =-v j , propagate v k = ⊥ = i-j if v i = v k , propagate v j = = ik if v i =-v k , propagate v j = ⊥ = i-k if v j = v k , propagate v i = = jk if v j =-v k , propagate v i = ⊥ = j-k if v i = , propagate v j = v k = i if v i = ⊥, propagate v j =-v k = i⊥ if v j = , propagate v i = v k = j if v j = ⊥, propagate v i =-v k = j⊥ if v k = , propagate v i = v j = k if v k = ⊥, propagate v i =-v j = k⊥
In our case, this simple mechanism of propagation is sufficient to establish that the formula is a tautology. We start with the state where v 11 = (-v 11 = ⊥) and apply the following rules:

v 11 = , we get v 7 = and v 10 = by & i on (7) v 7 = , we get v 5 = ⊥ and v 6 = ⊥ by & i on (3) v 10 = , we get v 8 = and v 9 = ⊥ by & i on (6) v 8 = , we get v 1 = and v 3 = by & i on (4) v 1 = , we get v 5 = -v 2 by & j on (1) v 2 = , we get v 9 = v 4 by & j on (5) v 3 = , we get v 6 = -v 4 by & j on (2)
The last equation is a contradiction since we know that v 6 = ⊥ and v 4 = v 9 = ⊥. Note that the order in which propagation rules are selected is arbitrary. Most of the time the propagation alone is not sufficient to conclude. In that case the dilemma rule can be applied. This rule works as depicted in Figure 2. Given a state S, it takes two arbitrary variables v i and v j and creates two In the second branch it adds the equation v i = -v j to get S 2 . On each of these branches, the propagation is applied to obtain S 3 and S 4 respectively. Then the result of the dilemma rule is the intersection S of S 3 and S 4 that contains all the equations that are valid independently of the relation between v i and v j . If one of the branches gives a contradiction, the result is the final state of the other branch. If we obtain a contradiction on both branches, a contradiction is reached. The dilemma rule is iterated on all pairs of variables taking the state resulting from the previous application as the initial state of the next one, till no new information is gained or a contradiction is reached. If no contradiction is reached, the same process is applied using four variables creating four branches

(v i = v j , v k = v l ), (v i = v j , v k = -v l ), (v i = -v j , v k = v l ) and (v i = -v j , v k = -v l )
). If the iteration on four variables is not sufficient to conclude, we can proceed using 6 then 8, . . . , then 2 * n variables. This gives us a generalized schema of the dilemma rule as depicted in Figure 3. The nice property of this algorithm is that the dilemma rule with four variables v i , v j , v k and v l with the restriction that v j = v l = is sufficient to find most of the tautologies occurring in formal verification.

Triplets

To define triplets in Coq we first need a notion of signed variables. For this, we introduce the type rZ with two constructors on nat: + and -. We also take the convention that is represented by +0 and ⊥ by -0. On rZ, we define the usual operations: complement (-), absolute value (||) and an order < such that i < j if and only if |i| < |j|.

A triplet is a set of three signed variables and a binary operation. We define the new type triplet with the only constructor Triplet:

Inductive triplet : Set := Triplet : rBoolOp → rZ → rZ → rZ → triplet
where rBoolOp is an enumerate type containing the two elements rAnd and rEq. In the following we use the usual pretty-printing convention for triplets: (Triplet rAnd i j k) and (Triplet rEq i j k) are written as i := j & k and i := j = k respectively. In order to define an evaluation on triplets, we first need to define an evaluation on rZ as:

Definition rZEval : (nat → bool ) → rZ → bool := λf: nat → bool . λr: rZ . Cases r of (+ n) =⇒ (f n) | (-n) =⇒ ¬(f n) end.
For the triplet we simply check that the first variable is equal to the result of applying the boolean operation to the other two variables:

Definition tZEval : (nat → bool ) → triplet → bool := λf: nat → bool . λt: triplet . Cases t of (Triplet r v 1 v 2 v 3 ) =⇒ (rZEval v 1 ) = ((rBoolOpFun r) (rZEval v 2 ) (rZEval v 3 )) end.
where the function rBoolOpFun maps elements of rBoolOp into their corresponding boolean operation.

As the algorithm manipulates a list of triplets, we introduce the notion of realizability: a valuation realizes a list of triplets if the evaluation of each triplet in the list gives true:

Definition realizeTriplets : (nat → bool ) → (list triplet) → Prop := λf: (nat → bool ). λL: (list triplet). ∀t: triplet. t in L ⇒ (tZEval f t) = .
Another interesting notion is the one of valid equation with respect to a list of triplets. An equation i = j is valid if for every valuation f that realizes a list of triplets L, f gives the same value for i and j:

Definition validEquation : (list triplet) → rZ → rZ → Prop := λL: (list triplet). λp, q: rZ . ∀f : (nat → bool ). (realizeTriplets f L) ⇒ (f 0) = ⇒ (rZEval f p) = (rZEval f q).
The condition (f 0) = is here to keep the convention that (+ 0) represents . Not every list of triplets corresponds to a boolean expression. To express the notion of tautology on triplets we simply ask for the top variable of the generated list to be evaluated to true: Definition tTautology : Expr → Prop := λe: Expr .

Cases (makeTriplets e) of (l, s) =⇒ (validEquation l s ) end.

where Expr is the type representing boolean expressions and makeTriplets is the function that computes the list of triplets corresponding to a given expression and its top variable. With this definition, we have the following theorem:

Theorem TautoEquivtTauto: ∀e: Expr . (tautology e) ⇐⇒ (tTautology e).

where the predicate tautology defines the usual notion of tautology on boolean expressions.

States

All the operations of checking and adding equations are done with respect to a state. We have chosen to represent states as lists of pairs of signed variables.

Definition State: Set := (list rZ * rZ ).

The inductive predicate ∼ defines when two variables are equal: The logic of Coq is constructive. This means that the theorem ∀P: Prop. P ∨ ¬P is not valid. But instances of this theorem can be proved. In particular we have:

Inductive ∼ : State → rZ →
Theorem stateDec: ∀S: State. ∀a, b: rZ . a ∼ S b ∨ ¬(a ∼ S b).
The property of being a contradictory state is defined as:

Definition contradictory: State → Prop := λS: State. ∃a: rZ . a ∼ s -a.
Note that from the definition of ∼, it follows that in a contradictory state all equalities are valid. Inclusion and equality on states are defined as:

Definition ⊂ : State → State → Prop := λS 1 , S 2 : State. ∀a, b: rZ . a ∼ S1 b ⇒ a ∼ S2 b. Definition ≡ : State → State → Prop := λS 1 , S 2 : State. S 1 ⊂ S 2 ∧ S 2 ⊂ S 1 .
A valuation realizes a state if all the equations of the state are valid:

Definition realizeState : (nat → bool ) → State → Prop := λf: nat → bool . λS: State. ∀a, b: rZ . (a, b) in S ⇒ (rZEval f a) = (rZEval f b).
We also need to define two basic functions on states: intersection and union. The union of two states is simply the state given by the concatenation of the two lists. In the following we use the notation (a, b)+S to denote [(a, b)] ∪ S.

The intersection of two states is not the intersection of their lists 1 . The function that computes the intersection of S 1 and S 2 first generates the list of all non-trivial equations of S 1 , i.e. all pairs (a,b) such that a ∼ S1 b and (a = b). Then, it removes from this list the equations that are not valid in S 2 . The resulting list represents S 1 ∩ S 2 .

One-step propagation

We formalize the one-step propagation as an inductive predicate → whose definition is given in Appendix A. Note that S 1 → t S 2 only means that there exists a rule that produces S 2 from S 1 using the triplet t. Because → is defined as a predicate, no particular strategy of rule application is assumed. The relation → is compatible with the equality as defined in Section 3.2:

Theorem →≡Ex : ∀S 1 , S 2 , S 3 : State. ∀t: triplet. S 1 → t S 2 ⇒ S 1 ≡ S 3 ⇒ ∃S 4 : State. S 3 → t S 4 ∧ S 4 ≡ S 2 .
Also a propagation only adds equations:

Theorem →∪Ex : ∀S 1 , S 2 : State. ∀t: triplet. S 1 → t S 2 ⇒ ∃S 3 : State. S 2 ≡ S 3 ∪ S 1 .
A corollary of this last theorem is that progatation always produces a bigger state:

Theorem →Incl : ∀S 1 , S 2 : State. ∀t: triplet. S 1 → t S 2 ⇒ S 1 ⊂ S 2 .
In a similar way we can prove that the relation behaves as a congruence:

Theorem →CongruentEx : ∀S 1 , S 2 , S 3 : State. ∀t: triplet. S 1 → t S 2 ⇒ ∃S 4 : State. (S 3 ∪ S 1 ) → t S 4 ∧ S 4 ≡ (S 3 ∪ S 2 ).
This gives us as a corollary that the relation is monotone:

Theorem →MonotoneEx : ∀S 1 , S 2 , S 3 : State. ∀t: triplet. S 1 → t S 3 ⇒ S 1 ⊂ S 2 ⇒ ∃S 4 : State. S 2 → t S 4 ∧ S 3 ⊂ S 4 .
Another interesting property is that the relation is confluent:

Theorem →ConflEx : ∀t 1 , t 2 : triplet. ∀S 1 , S 2 , S 3 : State. S 1 → t1 S 2 ⇒ S 1 → t2 S 3 ⇒ ∃S 4 , S 5 : State. S 2 → t2 S 4 ∧ S 3 → t1 S 5 ∧ S 4 ≡ S 5 .
Note that to establish these properties we do not use the particular equations that are checked or added. All relations with a shape similar to the one of → would have these properties.

The first semantic property that we have proved is that preserving the realizability for the one-step propagation is equivalent in some sense to evaluating the triplet to :

Theorem realizeStateEvalEquiv : ∀f: nat → bool . ∀S 1 , S 2 : State. ∀t: triplet. (f 0 ) = ⇒ (realizeState f S 1 ) ⇒ S 1 → t S 2 ⇒ ((realizeState f S 2 ) ⇐⇒ (tEval f t) = ).
Another key semantic property is that no matter which rule is applied, the resulting state is the same:

Theorem →Eq: ∀t: triplet. ∀S 1 , S 2 , S 3 : State. S 1 → t S 2 ⇒ S 1 → t S 3 ⇒ S 2 ≡ S 3 .
Moreover, a triplet is essentially useful only once:

Theorem →Invol : ∀t: triplet. ∀S 1 , S 2 , S 3 , S 4 : State. S 1 → t S 2 ⇒ S 2 ⊂ S 3 ⇒ S 3 → t S 4 ⇒ S 3 ≡ S 4 .
The proofs of the above theorems are not very deep and mostly involve exploring the twenty-one possible rules of one-step propagation.

Propagation

The propagation consists in iterating the one-step propagation. We take the reflexive transitive closure of → t :

Inductive → * : State → (list triplet) → State → Prop := → * Ref : ∀S 1 , S 2 : State. ∀L: (list triplet ). S 1 ≡ S 2 ⇒ S 1 → * L S 2 | → * Trans : ∀S 1 , S 2 , S 3 : State. ∀L: (list triplet). ∀t: triplet. t in L ⇒ S 1 → t S 2 ⇒ S 2 → * L S 3 ⇒ S 1 → * L S 3 .
All the properties of the one-step propagation can be lifted to the propagation. The exception is the theorem about realizability which has a simple implication since the propagation might use a strict subset of the list of triplets:

Theorem realizeStateEval * : ∀f: nat → bool . ∀S 1 , S 2 : State. ∀L: (list triplet ). (f 0 ) = ⇒ (realizeState f S 1 ) ⇒ S 1 → * L S 2 ⇒ (realizeTriplets f L) ⇒ (realizeState f S 2 ).
Finally the property that a triplet is useful only once is captured by:

Theorem → * TermEx : ∀L: (list triplet ). ∀S 1 , S 2 : State. S 1 → * L S 2 ⇒ (S 1 ≡ S 2 ) ∨ (∃t: triplet. ∃S 3 : State. t in L ∧ S 1 → t S 3 ∧ S 3 → * L-[t] S 2 ).
where L -[t] denotes the list obtained by removing t from L.

The dilemma rule

As we did for propagation, the dilemma rule is non-deterministic and modeled by a predicate. Also, we allow an arbitrary (but finite) number of splits:

Inductive → d : State → (list triplet) → State → Prop := → d Ref : ∀S 1 , S 2 : State. ∀L: (list triplet ). S 1 → * L S 2 ⇒ S 1 → d L S 2 | → d Split : ∀a, b: rZ . ∀S 1 , S 2 , S 3 , S 4 : State. ∀L: (list triplet ). ∀t: triplet. (a, b)+S 1 → d L S 2 ⇒ (a, -b)+S 1 → d L S 3 ⇒ S 2 ∩ S 3 ≡ S 4 ⇒ S 1 → d L S 4 .
The relation → d is compatible with the equality:

Theorem → d ≡ : ∀S 1 , S 2 , S 3 , S 4 : State. ∀L: (list triplet). S 1 → d L S 2 ⇒ S 3 ≡ S 1 ⇒ S 4 ≡ S 2 ⇒ S 3 → d L S 4 .
The same theorems about inclusion also hold:

Theorem → d ∪Ex : ∀S 1 ,
∩ S 2 ) ∪ S 3 ⊂ (S 1 ∪ S 3 ) ∩ (S 2 ∪ S 3 ) and not (S 1 ∩ S 2 ) ∪ S 3 ≡ (S 1 ∪ S 3 ) ∩ (S 2 ∪ S 3
), the relation is not a congruence. A simple way to recapture this congruence would be to define → d as:

Inductive → d : State → (list triplet) → State → Prop := → d Ref : ∀S 1 , S 2 : State. ∀L: (list triplet ). S 1 → * L S 2 ⇒ S 1 → d L S 2 | → d Split : ∀a, b: rZ . ∀S 1 , S 2 , S 3 , S 4 : State. ∀L: (list triplet ). ∀t: triplet. (a, b)+S 1 → d L S 2 ⇒ (a, -b)+S 1 → d L S 3 ⇒ S 1 ⊂ S 4 ⊂ (S 2 ∩ S 3 ) ⇒ S 1 → d L S 4
. but this would mean considering the merging of the two branches as a nondeterministic operation, so we prefer our initial definition. Even though the relation is not a congruence, it is monotone:

Theorem → d Monotone: ∀L: (list triplet ). ∀S 1 , S 2 , S 3 : State. S 1 → d L S 3 ⇒ S 1 ⊂ S 2 ⇒ ∃S 4 : State. S 2 → d L S 4 ∧ S 3 ⊂ S 4
. and it is also confluent:

Theorem → d Confluent: ∀L: (list triplet ). ∀S 1 , S 2 , S 3 : State. S 1 → d L S 2 ⇒ S 1 → d L S 3 ⇒ ∃S 4 : State. S 2 → d L S 4 ∧ S 3 → d L S 4 .
The last property we have proved about the dilemma rule is that it preserves realizability:

Theorem realizeStateEval d : ∀f: nat → bool . ∀S 1 , S 2 : State. ∀L: (list triplet ). (f 0 ) = ⇒ (realizeState f S 1 ) ⇒ S 1 → d L S 2 ⇒ (realizeTriplets f L) ⇒ (realizeState f S 2 ).

Stålmarck's algorithm

Stålmarck's algorithm is the reflexive transitive closure of the dilemma rule:

Inductive → s : State → (list triplet) → State → Prop := → s Ref : ∀S 1 , S 2 : State. ∀L: (list triplet). S 1 ≡ S 2 ⇒ S 1 → s L S 2 | → s Trans : ∀S 1 , S 2 , S 3 : State. ∀L: (list triplet). S 1 → d L S 2 ⇒ S 2 → s L S 3 ⇒ S 1 → s L S 3 .
As for → d we get the standard properties:

Theorem → s ≡ : ∀S 1 ,
(f 0 ) = ⇒ (realizeState f S 1 ) ⇒ S 1 → s L S 2 ⇒ (realizeTriplets f L) ⇒ (realizeState f S 2 ).
Only the last property is relevant for the correctness of the algorithm. From the theorem realizeStateEval s , the following property is easily derived: This is proved by showing that if e is a tautology, we obtain a contradiction by applying the dilemma rule on all the variables in the list of triplets. The program extracted from the constructive proof of the theorem stålmarckComplete would then not be faster than the one that computes the truth table.

Trace

Our relation → s contains all possible execution paths. The choice of the rules, the choice of the triplets and the choice of the variables for the dilemma rule are not explicitly given. A natural question arises on what an explicit implementation should produce to provide a certificate that it has reached a contradiction. Of course, a complete trace of the execution (states, rules, triplets, variables) is a valid certificate. In fact, we can do much better and keep only the triplets that have been used and the variables on which the dilemma rule has been applied. We define our notion of trace as:

Inductive Trace: Set := emptyTrace : Trace | tripletTrace : triplet → Trace | seqTrace : Trace → Trace → Trace | dilemmaTrace : rZ → rZ → Trace → Trace → Trace.
The semantics is given by the following predicate that evaluates a trace:

Inductive evalTrace: State → Trace → State → Prop := emptyEval : ∀S 1 , S 2 : State. S 1 ≡ S 2 ⇒ (evalTrace S 1 emptyTrace S 2 ) | tripletEval : ∀S 1 , S 2 : State. ∀t: triplet. S 1 → t S 2 ⇒ (evalTrace S 1 (tripletTrace t) S 2 ) | seqEval : ∀S 1 , S 2 , S 3 : State. ∀T 1 , T 2 : Trace. (evalTrace S 1 T 1 S 2 ) ⇒ (evalTrace S 2 T 2 S 3 ) ⇒ (evalTrace S 1 (seqTrace T 1 T 2 ) S 3 ) | dilemmaEval : ∀S 1 , S 2 , S 3 , S 4 : State. ∀a, b: rZ . ∀T 1 , T 2 : Trace. (evalTrace (a, b)+S 1 T 1 S 2 ) ⇒ (evalTrace (a, -b)+S 1 T 2 S 3 ) ⇒ S 2 ∩ S 3 ≡ S 4 ⇒ (evalTrace S 1 (dilemmaTrace a b T 1 T 2 ) S 4 ).
The fact that a trace determines a unique computation up to state equality is asserted by the following theorem:

Theorem evalTraceEq: ∀S 1 , S 2 , S 3 , S 4 : State. ∀T: Trace. (evalTrace S 1 T S 2 ) ⇒ (evalTrace S 3 T S 4 ) ⇒ S 1 ≡ S 3 ⇒ S 2 ≡ S 4 .
Conversely it is possible to get a trace from any non-deterministic computation:

Theorem stålmarckExTrace: ∀S 1 , S 2 : State. ∀L: (list triplet). S 1 → s L S 2 ⇒ ∃T: Trace. (evalTrace S 1 T S 2 ) ∧ T in L.
The second condition requires all the triplets in the trace T to be in L.

Implementation

Because of space limitation, we are only going to sketch the different components of the implementation. In particular, we do not make explicit the rules of sign using the notation ±v to denote either +v or -v.

Memory

We represent non-contradictory states using functional arrays. Appendix B lists the different axioms we are using in our development. The size of the array is maxN , the natural number that exceeds by at least one all the variables in the list of triplets. The type of the elements of the array is defined as follows:

Inductive vM : Set := ref : rZ → vM | class : (list rZ ) → vM
The value of the location i depends on the smallest element a such that +i ∼ a. Checking equality Given a memory m, it is easy to build a function min m that returns for any element a of rZ the smallest b such that a ∼ m b. To check the equality between a and b in m, it is then sufficient to compare (min m a) and (min m b).

Adding an equation Given a memory m, it is also easy to build a function l m that returns for any element a of rZ the ordered list of all the elements b such that a ∼ m b. The result of an addition to a memory is a triple (Mem, bool , (list rZ)). Since a memory can only represent a non-contradictory state, the boolean is set to true if the addition of the equation gives a contradiction, to false otherwise. The absolute values of the elements of the list are the locations of the arrays that have been modified by the update.

Propagation

The implementation of the one-step propagation is a composition of checking equalities and adding equations. It has the type Mem → triplet →(Mem, bool, (list rZ)). To do the propagation, we need to define a way to select triplets. As the difference lists give the variables whose values have been modified, triplets containing these variables are good candidate for applying onestep propagation. The type of the propagation function is Mem → (list rZ ) → (Mem, bool , (list rZ )). The difference lists resulting from the application of the one-step propagation are then recursively used for selecting triplets. This way of propagating terminates since we cannot add infinitely many equations to a memory.

Dilemma

We have implemented only the instances of the dilemma rule that are of practical use: dilemma1, the dilemma with (a, ) for an arbitrary a, and dilemma2, the dilemma with ((a, ), (b, )) for arbitrary a and b. To perform the first one, we use three memories, one for each branch and one to compute the intersection. For the second one we use an extra memory. The first memory m 1 is used to compute each branch iteratively. The intermediate result is stored in the second memory m 2 . At the end of each iteration we compute the intersection of m 1 and m 2 using the third memory m 3 . We then switch m 2 and m 3 and use the last memory to reset m 1 and m 3 before proceeding to the next branch. Note that a dilemma with any number of variables could be implemented in the same way using four memories.

Stålmarck

At this stage, we have to decide the strategy to pick up variables for the application of the dilemma rules. Our heuristics are very simple and could be largely improved. We first add the initial equation and propagate. If no contradiction is reached, we iterate the application of the function dilemma1 using minimal variables starting from +1 to +maxN . We perform this operation till a contradiction is reached or no more information is gained. In the second case, we do a double iteration with a, b such that 0 < a < b < maxN using the function dilemma2. Implementing this nave strategy is straightforward and gives us the function doStal for which we have proved the following property: Note that it is the only property that we have proved for our implementation and clearly it is not sufficient. An algorithm that always returns ⊥ would satisfy the above property. While our implementation is not complete since we use dilemma rules only up to four variables, we could prove some liveness property. This is feasible and would require to formalize the notion of n-hard formulae as described in [START_REF] Sheeran | A tutorial on Stålmarck's proof procedure for propositional logic[END_REF].

Benchmark

Once the implementation has been proved correct in Coq, the extraction mechanism [START_REF] Paulin-Mohring | Synthesis of ML programs in the system Coq[END_REF] enables us to get a functional Ocaml [START_REF] Leroy | Objective Caml[END_REF] program. The result is 1400 lines long. To be able to run such a program, we need to provide an implementation of the arrays that satisfies the axioms of Appendix B. A first possibility is to use balanced trees to implement functional arrays. A second possibility is to use tagged arrays, since we have taken a special care in the implementation in order to be able to use destructive arrays. The tag in the array prohibits illegal accesses. For example, the set function for such arrays looks like: If the program terminates without exception, the result is correct. Table 4 gives some execution times on standard examples taken from [START_REF] Harrison | Stålmarck's algorithm as a HOL derived rule[END_REF]. For each problem, we give which level of dilemma rules is needed, the number of variables, the number of connectives and compare three versions of the algorithm: the algorithm is directly hand-coded in Ocaml with slightly different heuristics, our certified version with balanced trees and with tagged arrays. The time includes parsing the formula and generating triplets. Even though the performance of an implementation largely depends on the heuristics, our certified version seems comparable with the hand-coded one and the one presented by John Harrison in [START_REF] Harrison | Stålmarck's algorithm as a HOL derived rule[END_REF]. However, we are aware that in order to get a realistic implementation, much more work on optimizations and heuristics has to be done.

Conclusion

We hope that what we have presented shows that current theorem proving technology can be effectively used to reason about algorithms and their implementations. We have presented a formalization of Stålmarck's algorithm that includes formal proofs of the main properties of the algorithm. Then, we have proposed a format of execution traces and proved that it is adequate. Such certificates are important in practice. They represent a simple way of increasing the confidence in the correctness of specific results. Prover Technology that commercializes a tool based on Stålmarck's algorithm has defined its own format of traces [START_REF] Jonasson | Proof logging, definition of the log format[END_REF]. John Harrison [START_REF] Harrison | Stålmarck's algorithm as a HOL derived rule[END_REF] also presents a tactic based on Stålmarck's method for HOL [START_REF] Michael | Introduction to HOL : a theorem proving environment for higher-order logic[END_REF] using traces: the search is handled by a program that generates traces, then, the prover uses these traces to build safe derivations of theorems. Finally, the effort for deriving a certified implementation is orthogonal to the one on traces since the correctness of results is ensured once and for all. The benchmarks given in Section 5.5 show that our implementation is relatively efficient and can be proposed as a reference implementation.

From the point of view of theorem proving, the most satisfying aspect of this work is the formalization of the algorithm. It is a relatively concise development of 3200 lines including 80 definitions and 200 theorems. The proof of correctness of the implementation is less satisfying. Proving the basic operations (addition and intersection) took 2/3 of the effort and represents more than 6000 lines of Coq. This does not reflect the effective difficulty of the task. The main reason why deriving these basic operations has been so tedious is that most of the proofs involves a fair amount of case-splitting. For example, proving properties of the addition often requires to take into account the signs and the relative value of the components of the equation. We have neither managed to abstract our theorems enough nor got enough automation so that we do not have to operate on the different cases manually. Moreover, the fact that we handle imperative features such as arrays in a functional way is a bit awkward. We plan in a near future to use improvements such those presented in [START_REF] Filliâtre | Proof of Imperative Programs in Type Theory[END_REF] to reason directly on imperative programs inside Coq. Finally while the overall experience is quite positive, we strongly believe that for this kind of formalization to become common practice, an important effort has to be done in order to make proofs scripts readable by non-specialists. In that respect, recent efforts such as [START_REF] Coscoy | Extracting text from proofs[END_REF][START_REF] Syme | Three Tactic Theorem Proving[END_REF][START_REF] Wenzel | A Generic Interpretative Approach to Readable Formal Proof Documents[END_REF][START_REF] Zammit | On the Implementation of an Extensible Declarative Proof Language[END_REF] seem very promising.

Fig. 2 .Fig. 3 .

 23 Fig. 2. The dilemma rule

  rZ → Prop := ∼Ref : ∀a: rZ . ∀S: State. a ∼ S a | ∼In : ∀a, b: rZ . ∀S: State. (a, b) in S ⇒ a ∼ S b | ∼Sym : ∀a, b: rZ . ∀S: State. a ∼ S b ⇒ b ∼ S a | ∼Inv : ∀a, b: rZ . ∀S: State. a ∼ S b ⇒ -a ∼ S -b | ∼Trans : ∀a, b, c: rZ . ∀S: State. a ∼ S b ⇒ b ∼ S c ⇒ a ∼ S c | ∼Contr : ∀a, b, c: rZ . ∀S: State. a ∼ S -a ⇒ b ∼ S c.

  Theorem stålmarckValidEquation: ∀L: (list triplet ). ∀a, b: rZ . ∀S: State. [(a, -b)] → s L S ⇒ (contradictory S) ⇒ (validEquation L a b). Once we have this theorem, we can glue together all the theorems about tautology to get the correctness: Theorem stålmarckCorrect: ∀e: Expr . ∀S: State. Cases (makeTriplets e) of (l, s) =⇒ [(s, ⊥)] → s l S ⇒ (contradictory S) ⇒ (Tautology e) end. Another property that has been formalized is the completeness of the algorithm: Theorem stålmarckComplete: ∀e: Expr . (Tautology e) ⇒ ∃S: State. Cases (makeTriplets e) of (l, s) =⇒ [(s, ⊥)] → s l S ∧ (contradictory S) end.

  If i = |a|, the location i contains the value (ref a). Otherwise, it contains the value (class L), where L is the ordered list of the elements b such that +i ∼ b and |b| = i. All the constraints about the different values of the array are concentrated in the predicate WellFormed: Definition Mem: Set := {r : (Array maxN vM )| (WellFormed maxN r)}.

  To perform the addition of a = b to m, we first compare (min m a) and (min m b). If (min m a) = (min m b), the result is (m, ⊥, []). If (min m a) = -(min m b), the result is (m, , []). If (min m a) < (min m b), the result is (m , ⊥, [(min m a)] ∪ (l m b)) where m is obtained from m by setting the locations corresponding to the elements of (l m b) to (ref ± (min m a)) and the location |(min m a)| to (class (±(l m a)∪±(l m b))). The case where (min m b) < (min m a) is symmetric to the previous one. Intersection The function that computes the intersection takes three memories m 1 , m 2 , m 3 and two lists d 1 , d 2 under the hypothesis that m 1 ⊂ m 2 , m 1 ⊂ m 3 , d 1 is the difference list between m 1 and m 2 , and d 2 is the difference list between m 1 and m 3 . It returns a 4-tuple (m 1 , m 2 , m 3 , d ) such that m 1 = m 2 ∩ m 3 , m 1 ≡ m 2 ≡ m 3 and d is the difference list between m 1 and m 1 . It proceeds by successive additions to m 1 of equations a i = b i where the a i are the elements of d 1 ∩ d 2 and the b i are the smallest element such that a i ∼ m2 b i and a i ∼ m3 b i .

  Theorem doStalCorrect: ∀e: Expr . (doStal e) = ⇒ (Tautology e).

  ∀S 1 , S 2 , S 3 : State. S 1 → s L S 2 ⇒ S 1 → s L S 3 ⇒ ∃S 4 : State. S 2 → s L S 4 ∧ S 3 → s L S 4 .

	Theorem realizeStateEval

S 2 , S 3 , S 4 : State. ∀L: (list triplet). S 1 → s L S 2 ⇒ S 3 ≡ S 1 ⇒ S 4 ≡ S 2 ⇒ S 3 → s L S 4 . Theorem → s ∪Ex : ∀S 1 , S 2 : State. ∀L: (list triplet ). S 1 → s L S 2 ⇒ ∃S 3 : State. S 2 ≡ S 3 ∪ S 1 . Theorem → s Incl : ∀S 1 , S 2 : State. ∀L: (list triplet). S 1 → s L S 2 ⇒ S 1 ⊂ S 2 . Theorem → s Monotone: ∀L: (list triplet ). ∀S 1 , S 2 , S 3 : State. S 1 → s L S 3 ⇒ S 1 ⊂ S 2 ⇒ ∃S 4 : State. S 2 → s L S 4 ∧ S 3 ⊂ S 4 . Theorem → s Confluent: ∀L: (list triplet ). s : ∀f: nat → bool . ∀S 1 , S 2 : State. ∀L: (list triplet ).

For example, given the lists [(1,

2);[START_REF] Coscoy | Extracting text from proofs[END_REF][START_REF] Filliâtre | Proof of Imperative Programs in Type Theory[END_REF]] and [(1, 3)], their intersection as states is [(1, 3)] while their intersection as lists is [].

-r ⇒ S → p:=q & r (q, ⊥)+(r , )+S :=q & r (p, r )+S | → & q-r : ∀p, q, r: rZ . ∀S:

→ =pq : ∀p, q, r: rZ . ∀S: State. p ∼ S q ⇒ S → p:=q=r (r , )+S | → = p-q : ∀p, q, r: rZ . ∀S: State. p ∼ S -q ⇒ S → p:=q=r (r , ⊥)+S | → =pr : ∀p, q, r: rZ . ∀S: State. p ∼ S r ⇒ S → p:=q=r (q, )+S | → = p-r : ∀p, q, r: rZ . ∀S: State. p ∼ S -r ⇒ S → p:=q=r (q, ⊥)+S | → =qr : ∀p, q, r: rZ . ∀S: State. q ∼ S r ⇒ S → p:=q=r (p, )+S | → = q-r : ∀p, q, r: rZ . ∀S: State. q ∼ S -r ⇒ S → p:=q=r (p, ⊥)+S | → = p : ∀p, q, r: rZ . ∀S: State. p ∼ S ⇒ S → p:=q=r (q, r ))+S | → = p⊥ : ∀p, q, r: rZ . ∀S: State. p ∼ S ⊥ ⇒ S → p:=q=r (q, -r )+S | → = q : ∀p, q, r: rZ . ∀S: State. q ∼ S ⇒ S → p:=q=r (p, r )+S | → = q⊥ : ∀p, q, r: rZ . ∀S: State. q ∼ S ⊥ ⇒ S → p:=q=r (p, -r )+S | → = r : ∀p, q, r: rZ . ∀S: State. :=q=r (p, -q)+S .


Azrul Abdullah

Ku Nor

Izah Ku

Norshamshina Mat

Risk Management Committee and Disclosure of Hedging Activities Information Among Malaysian Listed Companies

Keywords: Financial Instruments, Hedging Activities, Disclosure Index, Risk Management Committee

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

The introduction of IFRS 7 (Financial Instruments: Disclosure) is argued to be able to enhance the disclosure of derivatives and hedging activities information. On the Malaysian scene, FRS 7 (Financial Instruments: Disclosures), now MFRS 7, has been made effective from Jan 1, 2010. MFRS 7 which is based on IFRS 7, segregates IAS 32 (the Malaysian equivalent of FRS 132: Financial Instruments: Disclosure and Presentation). It provides an overview of the entity's use of derivatives and the exposure to risks they create. While MFRS 7 has just been applied by business entities in Malaysia, several studies in other countries have raised concerns regarding the extent and quality of the derivatives disclosure provided by companies in meeting this accounting standard [see 1, 2, 3 and 4] particularly on the hedging activities information.

It was claimed that the derivatives disclosure was less useful and subject to management discretion [see 5, 6, and 7]. Moreover, since hedge accounting is optional, companies may use their discretion not to report the use of derivatives for hedging activities5. Several studies Please quote this paper as Abdullah, A., Ismail provide evidence that companies avoid full compliance in disclosing their hedging activities information in annual reports [see, [START_REF] Hassan | The Transparency of Derivative Disclosures by Australian Firms in the Extractive Industries[END_REF][START_REF] Bamber | An examination of voluntary financial instruments disclosures in excess of mandatory requirements by UK FTSE 100 non-financial firms[END_REF][START_REF] Papa | User Perspectives on Financial Instrument Risk Disclosures under Derivatives and Hedging Activities Disclosures[END_REF]. In this respect, some studies propose that one of the important elements that should exist in a company for a better transparency of derivatives and hedging activities disclosure is the establishment of Risk Management Committees (RMCs)

[see [START_REF] Hassan | The Transparency of Derivative Disclosures by Australian Firms in the Extractive Industries[END_REF][START_REF] Hassan | Risk Management Committee and Financial Instrument Disclosure[END_REF][START_REF] Birt | Derivatives use and financial instrument disclosure in the extractives industry[END_REF]. Nevertheless, there are mixed empirical evidences justifying the existence of RMCs and the degree of transparency and quality of financial instruments disclosure, particularly on the derivatives and hedging activities information1, 8, 9. Thus, it is the objective of this study to examine the effectiveness of RMCs. Different from earlier studies, this study focuses on the characteristics of RMCs as a proxy for its effectiveness (i.e. size, independence, meeting, diversity and training). This paper is outlined as follows: Section 2 highlights related Malaysian studies on financial instruments disclosure. Section 3 shows the hypotheses of this study. Section 4 explains the methodology and Section 5 presents the results. Lastly, Section 6 concludes this paper.

MALAYSIAN RELATED STUDIES

In Malaysia, limited studies were found to address the disclosure of financial instruments information [see [START_REF] Hassan | Risk Management Committee and Financial Instrument Disclosure[END_REF][START_REF] Abdullah | The Association between Committees Responsible for Risk Management and the Disclosure Level of Financial Instruments Information among Listed Companies in Malaysia[END_REF][START_REF] Ng | Is the risk management committee only a procedural compliance? An insight into managing risk taking among insurance companies in Malaysia[END_REF][START_REF] Adznan | Financial Instruments Disclosure Practices: Evidence from Malaysia Listed Firms[END_REF]. The earliest traceable study that provides evidence of the extent of financial instruments disclosure (including derivatives) only relates to two specific company characteristics, which are company size, and the level of foreign activities. Moreover, the study also claims that the level of disclosure of derivatives before the issuance of the accounting standard is low, possibly due to the lack of control mechanisms in Malaysia. In addition, the results of the study has been argued to be bias since the disclosure is voluntary in nature and certain companies might have different capabilities in terms of money and human resources.

In another study6, it was reported that the existence of the risk management committee (RMC), company size, and profitability are associated with high quality financial instruments information. Although it provides some meaningful insights, the study is still not conclusive as the results may be outdated. The study was conducted in the period before the revised accounting standard for financial instruments was issued. Moreover, in recent studies [START_REF] Abdullah | The Association between Committees Responsible for Risk Management and the Disclosure Level of Financial Instruments Information among Listed Companies in Malaysia[END_REF], [START_REF] Adznan | Financial Instruments Disclosure Practices: Evidence from Malaysia Listed Firms[END_REF], it is found that RMCs has no relationship with the extent of derivatives disclosure while audit committees have more influence on the extent of the disclosure [START_REF] Adznan | Financial Instruments Disclosure Practices: Evidence from Malaysia Listed Firms[END_REF]. It is argued that this may be due to the lack of independence and effectiveness of RMCs.

Please quote this paper as Abdullah, A., Ismail

HYPOTHESES

This study uses agency theory and resource dependency theory as underpinning theories to develop the hypotheses [see, [START_REF] Jensen | Theory of the firm: managerial behavior, agency costs and ownership structure[END_REF][START_REF] Pfeffer | The external control of organisations: A resource dependence perspective[END_REF][START_REF] Erakovic | Board-management relationships: resources and internal dynamics[END_REF]. The following hypotheses have been developed in this study:

H1:

The extent of hedging activities information disclosure is positively associated with RMC size.

H2:

The extent of hedging activities information is positively associated with RMC independence H3: The extent of hedging activities information is positively associated with RMC meeting.

H4:

The extent of hedging activities information is positively associated with the proportion of female directors on RMCs.

H5:

The extent of hedging activities information is positively associated with the number of risk management training attended by RMC members.

RESEARCH METHODOLOGY

This study uses secondary data, collected from two separate sources which are DataStream and the Malaysian listed companies' annual report, downloaded from the Bursa Malaysia's website.

Financial data (i.e. ROA, total assets and leverage) are obtained from the Datastream.

Information on the risk management committees is gathered from the board of directors' profile and risk management report section in the annual reports. In the case where RMC is a subcommittee of the audit committee (AC), this study selects the RMC characteristics based on AC characteristics. It is assumed valid as the establishment of an RMC through AC performs similar roles. Our sample comprises 300 largest companies listed on the Main Board of Bursa Malaysia in 2013. Companies that are in the sectors such as banking, insurance, trust, REITs and closed-end funds are omitted from the sample due to additional regulations imposed on them [START_REF] Hassan | Risk Management Committee and Financial Instrument Disclosure[END_REF][START_REF] Abdullah | Disclosure of voluntary ratios by Malaysian Listed Companies[END_REF]. This sample size is assumed sufficient because many previous financial instrument disclosure studies had shown that there is no specific rule that specifies the sample size [See, [START_REF] Hassan | The Transparency of Derivative Disclosures by Australian Firms in the Extractive Industries[END_REF][START_REF] Lopes | Accounting for financial instruments: An analysis of the determinants of disclosure in the Portuguese stock exchange[END_REF][START_REF] Abdullah | The Association between Committees Responsible for Risk Management and the Disclosure Level of Financial Instruments Information among Listed Companies in Malaysia[END_REF]. The 2013 financial year has been chosen because it is the third year MFRS 7 has been fully adopted. The time is sufficient for companies to adopt the standard. Nevertheless, we eventually ended up with 117 companies since not all the sampled companies use derivatives to evade their financial risk exposure and establish an RMC. The dependent variable of this study is the extent of hedging activities information disclosure (EHAD). To measure this variable, a disclosure index was prepared, based on 32 mandatory and discretionary disclosure items. The score is calculated by adding up all items disclosed divided by the maximum number of possible scores. Mandated disclosures on derivatives and hedge activities information are directly derived from MFRS 7 (Financial Instruments: Disclosure). Specifically, such disclosure items include all those in the hedge accounting section of MFRS 7 (paragraph 22-24) and other related hedging activities disclosure requirements. For voluntary hedging activities information, the disclosure items are extracted and composed from the accounting literature. In order to avoid unsystematic evaluation processes and the reliability of the design disclosure checklist, we further cross-check such disclosure items with the PWC's IFRS Presentation and Disclosure Checklist 2012. The PWC's disclosure checklist is used because it presents a practically tested auditing tool where this study assumed that high assurance on disclosure of hedging activities information can be counted on. Table 1 shows the measurements of the all the RMC characteristics and control variables.

Table.1. Measurement of Explanatory Variables

To test the relationship between RMC characteristics and the extent of hedging activities information disclosure, a multiple linear regression is performed. The regression model is constructed as follows:

Please quote this paper as Abdullah, A., Ismail

RESULTS AND DISCUSSIONS

Descriptive statistics for the variables is shown in Table 2. As evidenced from the table, there are variations in the disclosure of hedging activities information between sampled companies.

The mean score for the extent of hedging activities disclosure is 0.7729 with a minimum score of 0.44 and a maximum score of 0.98. The average of RSIZE is 3.83 members (approximately 4), exceeding the minimum demand of three members in AC. The largest RMC comprises 9 members while the smallest comprises 2 members. The mean score of 0.7082 for RINDE indicates that on average, the number of independent directors in RMCs is greater than nonindependent directors. In other words, RMCs in Malaysia are more likely to be independent, although it is voluntary in nature. Some of the RMCs comprise of all independent directors, while some have no independent director. On average, RMCs conduct their meetings 4 times a year; however, there are RMCs that did not conduct any RMC meeting. The highest number of meetings of the sampled companies is 12 times. The mean RDIVER of 0.32 shows that on average women represent 32 percent of the RMC.

Table.2. Descriptive Statistics

Table 3 presents the outcomes of the regression analysis between the disclosure of hedging activities information, RMC characteristics and control variables. The Variance Inflation Factor (VIF) statistics indicate that multicollinearity does not exist in the model as the values are less than 10. The model explains 21.1 percent of the variation in the level of hedging activities information disclosure, which is relatively low. Although the adjusted R2 is low, the finding is consistent with those of the previous studies, which pointed out that the low R2 is common in corporate governance researches [see, [START_REF] Hassan | The Transparency of Derivative Disclosures by Australian Firms in the Extractive Industries[END_REF][START_REF] Ng | Is the risk management committee only a procedural compliance? An insight into managing risk taking among insurance companies in Malaysia[END_REF][START_REF] Ismail | Institutional Investors and Board of Directors' Monitoring Role on Risk Management Disclosure Level in Malaysia[END_REF]. We provide some insights on the association between EHAD and each of RINDE, RMEET, CSIZE and LEV. Table 3 shows that RINDE (t value = -2.497) has a significant and negative relationship with the extent of hedging activities disclosure, at p < 0.01. This finding indicates that independent directors in RMCs are not concerned with the extent of hedging activities information disclosure. A possible explanation is that independent directors do not contribute their experience as well as their skills and knowledge towards increasing the information on hedging activities [see [START_REF] Ng | Is the risk management committee only a procedural compliance? An insight into managing risk taking among insurance companies in Malaysia[END_REF][START_REF] Ismail | Institutional Investors and Board of Directors' Monitoring Role on Risk Management Disclosure Level in Malaysia[END_REF]. As argued in the literature, independent directors do not play an active role in supervising the management as the directors usually rely on management for information due to their busy schedule and commitment towards other activities. Another possible explanation is that the independent directors may have a relationship with the management, making way for their long period of experience on the boards. As a result, their decision making may have been influenced by the management since their appointment to the board is merely due to their relationship with the company. Results from Table 3 also show that RMEET has a significant and positive relationship with the extent of hedging activities information disclosure. This indicates that frequent meetings by RMCs are more likely to be related to high level of hedging activities disclosure. However, RSIZE, RDIVER, RTRAIN and REXPERT are found insignificant.

Table.3. Regression Results

Please quote this paper as Abdullah, A., Ismail Consistent with prior research, company size was also found to be positively related to the extent of hedging activities information disclosure [see, [START_REF] Hassan | The Transparency of Derivative Disclosures by Australian Firms in the Extractive Industries[END_REF][START_REF] Lopes | Accounting for financial instruments: An analysis of the determinants of disclosure in the Portuguese stock exchange[END_REF][START_REF] Wei | Determinants of Fair Value Financial Instrument and Share-Based Payment Disclosure Patterns of Australian Listed Firms[END_REF][START_REF] Hassan | Risk Management Committee and Financial Instrument Disclosure[END_REF][START_REF] Ng | Is the risk management committee only a procedural compliance? An insight into managing risk taking among insurance companies in Malaysia[END_REF][START_REF] Ismail | Institutional Investors and Board of Directors' Monitoring Role on Risk Management Disclosure Level in Malaysia[END_REF]. Based on agency theory, large firms incur lower information processing costs, but higher political costs, thereby encouraging them to disclose greater information. With regard to audit quality, this study found that hedging activities disclosure is not significantly influenced by Big 4 audit firms6. PROF is found not to be related to EHAD. One factor that could explain the finding is the impact of the global systemic economic crisis (i.e. Eurozone debt and world petroleum price fluctuations). The recovery planning after the crisis that occurred during the period may affect the performance of the sampled companies. However, the prediction that the disclosure of hedging activities information is positively related to financial risks (i.e. leverage) is supported at p < 0.05. The result is consistent with some of the previous studies. The extent of disclosure increases with increasing financial risks, where companies with higher leverage increase disclosure to reduce potential agency costs associated with external funding and their asset replacement16.

CONCLUSION

The objective of this study is to examine the influence of risk management committee characteristics (i.e. RMC size, RMC independence, RMC meeting, RMC gender diversity and RMC training) to the extent of hedging activities information disclosures in the annual reports of Malaysian listed companies. The analysis shows that the RMC characteristics (i.e. RINDE, RMEET) have some significant bearing in influencing the extent of hedging activities information disclosure in Malaysia. Intrinsically, this finding may provide some meaningful insights to the regulator, policy makers and researchers, especially in incorporating RMCs as part of the corporate governance mechanisms. It is not just the existence of RMC, but their effectiveness is something that needs to be emphasized.

  Please quote this paper as Abdullah, A.,Ismail, K. N. I. K., & Isa, N. M. (2015). Risk Management Committee and Disclosure of Hedging Activities Information among Malaysian Listed Companies. Advanced Science Letters, 21(6), 1871-1874.

  Please quote this paper as Abdullah, A.,Ismail, K. N. I. K., & Isa, N. M. (2015). Risk Management Committee and Disclosure of Hedging Activities Information among Malaysian Listed Companies. Advanced Science Letters, 21(6), 1871-1874.

  , K. N. I. K., & Isa, N. M. (2015). Risk Management Committee and Disclosure of Hedging Activities Information among Malaysian Listed Companies. Advanced Science Letters, 21(6), 1871-1874.

  , K. N. I. K., & Isa, N. M. (2015). Risk Management Committee and Disclosure of Hedging Activities Information among Malaysian Listed Companies. Advanced Science Letters, 21(6), 1871-1874.

  , K. N. I. K., & Isa, N. M. (2015). Risk Management Committee and Disclosure of Hedging Activities Information among Malaysian Listed Companies. Advanced Science Letters, 21(6), 1871-1874.

  , K. N. I. K., & Isa, N. M. (2015). Risk Management Committee and Disclosure of Hedging Activities Information among Malaysian Listed Companies. Advanced Science Letters, 21(6), 1871-1874.

ACKNOWLEDGMENTS

Special thanks to Ministry of Education Malaysia, Universiti Teknologi Mara (UiTM) and Universiti Utara Malaysia (UUM).