In this paper we shall consider proofs of declarative properties of Definite Programs, i.e. properties associated with their logical semantics, in particular what is called the partial correctness of a logic program with respect to a specification and properties related to the proof theoretic semantics based on the notion of proof-tree. A specification consists of a logical formula associated with each predicate and establishing a relation between its arguments. A definite program is partially correct if every possible answer substitution satisfies the specification. This paper generalizes known results in logic programming in three ways : first it considers any kind of specification, second its results can be applied to extensions of logic programming such as functions or constraints, third new proof methods (the annotations methods) are presented. It gives an unified framework for different kind of known proof methods like the consequence verification method, the structural induction in definite clauses or the inductive proof of formulas. Two proof methods are presented. The second is adapted from the Attribute Grammar field to the field of Logic Programming. Both are proven sound and complete. The first one consists of defining a specification stronger than the original one, which furthermore is inductive (fixpoint induction). Many aspects of the inductive specification method are investigated.The second method is a refinement of the first one : with every predicate, one associates a finite set of formulas (we call this an annotation), together with implications between formulas. The proofs become more modular and tractable, but the user has to verify the consistency of his proof, which is a decidable property. This method is particularly suitable for proving the validity of specifications which are not inductive. It has the same power as the first method, but it is more specifically adapted to prove properties holding inside the proof-trees.