Transforming EVENT B Models into Verified C# Implementations