This paper proposes a formalization of the IFPUG Function Point (FP) definition for automated measurement of B specifications. This formal definition allows to: i) reduce the variance in FP counts due to rater interpretation of the IFPUG FP informal definition; ii) provide a better understanding of how the IFPUG FP definition should be applied; iii) automate the FP counts for B specifications, which can reduce measurement costs; and iv) identify specific holes in the IFPUG FP definition. We propose modifications to ensure completeness.