AdaCore Blog

10 entries tagged with #Java

by Pamela Trevino

Public Ada Training Paris, France Dec 3 - 7, 2018

This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.

by Fabien Chouteau, Emma Adby, Yannick Moy

Learn.adacore.com is here

We are very proud to announce the availability of our new Ada and SPARK learning platform learn.adacore.com, which will replace AdaCoreU(niversity) e-learning platform. Learn all about it in this blog post.

#Teaching    #Ada    #SPARK   

by Yannick Moy

Two Days Dedicated to Sound Static Analysis for Security

​AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they are used to increase the security of software-based systems. The program gathers top-notch experts in the field, from industry, government agencies and research institutes, around the three themes of analysis of legacy code, use in new developments and accountable software quality. Here is why it is worth attending.

#SPARK    #Frama-C    #Security    #Formal Methods    #Static Analysis   

by Felix Krause

The Road to a Thick OpenGL Binding for Ada: Part 1

This blog post is part one of a tutorial based on the OpenGLAda project and will cover some the background of the OpenGL API and the basic steps involved in importing platform-dependent C functions.

#OpenGL    #Binding   

by Quentin Ochem

Unity & Ada

Using Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.

#GitHub    #Ada    #GNAT    

by Martyn Pike

The latest Mixed Programming with Ada lectures at the AdaCore University

I recently joined AdaCore as a Technical Account Manager with an initial focus on the UK and Scandinavian regions, but for the last 12 months I've been busy working on the AdaCore University. The most recent addition to which is a course on Mixed Language Programming with Ada, and it includes lectures on the integration of Ada with C, C++ and Java. The course covers some advanced topics like mixed language object orientation, techniques for using Ada strong typing to combat known issue with C pointers and the pitfalls that are encountered when mixing native Ada code with Java at runtime. This course clearly demonstrates that Ada has strong support for integration with C, C++ and Java and it proves there are no technical barriers to its adoption in modern mixed language software systems.

#Mixed Language    #AdaCore University    #Java    #C++    #C    

by Yannick Moy

Studies of Contracts in Practice

Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts (Eiffel obviously, Java with JML contracts and C# with Code Contracts). I'm reporting what I found interesting (and less so) in these two studies.

#Language    #Formal Verification    #Contracts   

by Yannick Moy

SPARK 2014 Rationale: Mixing SPARK and Ada Code

The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification within the overall Ada application. This post presents the solution we've come up with for SPARK 2014.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Specification Functions

Specifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Yet, specification functions must obey specific constraints like absence of side-effects and termination, that have led to different solutions in various specification languages. Here is what we did in SPARK 2014.

#Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Contract Cases

Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a contract by cases. A little history helps understanding how we came up with this new feature.

#Formal Verification    #SPARK